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

State before:
⊢ denum (Univ ℚ)
Tactic:
set I : Set Nat := image fqn (Univ Rat)
State after:
I : Set ℕ := image fqn (Univ ℚ)
⊢ denum (Univ ℚ)

State before:
I : Set ℕ := image fqn (Univ ℚ)
⊢ denum (Univ ℚ)
Tactic:
have h1 : Univ Nat ∼ I := unbdd_subset_nat image_fqn_unbdd
State after:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
⊢ denum (Univ ℚ)

State before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
⊢ denum (Univ ℚ)
Tactic:
have h2 : image fqn (Univ Rat) = I := by rfl
State after:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
⊢ denum (Univ ℚ)

State before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
⊢ denum (Univ ℚ)
Tactic:
have h3 : Univ Rat ∼ I :=
  equinum_image (one_one_on_of_one_one fqn_one_one (Univ Rat)) h2
State after:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
h3 : Univ ℚ ∼ I
⊢ denum (Univ ℚ)

State before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
h3 : Univ ℚ ∼ I
⊢ denum (Univ ℚ)
Tactic:
have h4 : I ∼ Univ Rat := Theorem_8_1_3_2 h3
State after:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
h3 : Univ ℚ ∼ I
h4 : I ∼ Univ ℚ
⊢ denum (Univ ℚ)

State before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
h2 : image fqn (Univ ℚ) = I
h3 : Univ ℚ ∼ I
h4 : I ∼ Univ ℚ
⊢ denum (Univ ℚ)
Tactic:
show denum (Univ Rat) from Theorem_8_1_3_3 h1 h4
State after:
no goals

State before:
I : Set ℕ := image fqn (Univ ℚ)
h1 : Univ ℕ ∼ I
⊢ image fqn (Univ ℚ) = I
Tactic:
rfl
State after:
no goals