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

State before:
U : Type
F : Set (Set U)
h1 : ctble F
h2 : ∀ A ∈ F, ctble A
⊢ ctble (⋃₀ F)
Tactic:
obtain (f : Set U → Rel Nat U) (h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A)
  from Lemma_8_2_2_2 h2
State after:
U : Type
F : Set (Set U)
h1 : ctble F
h2 : ∀ A ∈ F, ctble A
f : Set U → Rel ℕ U
h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
⊢ ctble (⋃₀ F)

State before:
U : Type
F : Set (Set U)
h1 : ctble F
h2 : ∀ A ∈ F, ctble A
f : Set U → Rel ℕ U
h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
⊢ ctble (⋃₀ F)
Tactic:
show ctble (⋃₀ F) from Lemma_8_2_2_1 h1 h3
State after:
no goals