Theorem: HTPI.Theorem_8_1_5_3 (HTPILib/Chap8Part2.lean)

State before:
U : Type
A : Set U
⊢ ctble A ↔ ∃ R, fcnl_one_one_to_nat R A
Tactic:
apply Iff.intro
State after:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ R, fcnl_one_one_to_nat R A

case mpr
U : Type
A : Set U
⊢ (∃ R, fcnl_one_one_to_nat R A) → ctble A

State before:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ R, fcnl_one_one_to_nat R A
Tactic:
assume h1 : ctble A
State after:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ R, fcnl_one_one_to_nat R A

State before:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
have h2 : ∃ (R : Rel Nat U), fcnl_onto_from_nat R A :=
  Theorem_8_1_5_1_to_2 h1
State after:
case mp
U : Type
A : Set U
h1 : ctble A
h2 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ R, fcnl_one_one_to_nat R A

State before:
case mp
U : Type
A : Set U
h1 : ctble A
h2 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
show ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A from
  Theorem_8_1_5_2_to_3 h2
State after:
no goals

State before:
case mpr
U : Type
A : Set U
⊢ (∃ R, fcnl_one_one_to_nat R A) → ctble A
Tactic:
assume h1 : ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A
State after:
case mpr
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
⊢ ctble A

State before:
case mpr
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
⊢ ctble A
Tactic:
show ctble A from Theorem_8_1_5_3_to_1 h1
State after:
no goals