Metamath Proof Explorer

Theorem tz9.12

Description: A set is well-founded if all of its elements are well-founded. Proposition 9.12 of TakeutiZaring p. 78. The main proof consists of tz9.12lem1 through tz9.12lem3 . (Contributed by NM, 22-Sep-2003)

Ref Expression
Hypothesis tz9.12.1 ⊢ A ∈ V
Assertion tz9.12 ⊢ ∀ x ∈ A ∃ y ∈ On x ∈ R1 ⁡ y → ∃ y ∈ On A ∈ R1 ⁡ y

Proof

Step Hyp Ref Expression
1 tz9.12.1 ⊢ A ∈ V
2 eqid ⊢ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v = z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v
3 1 2 tz9.12lem2 ⊢ suc ⁡ ⋃ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v A ∈ On
4 3 onsuci ⊢ suc ⁡ suc ⁡ ⋃ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v A ∈ On
5 1 2 tz9.12lem3 ⊢ ∀ x ∈ A ∃ y ∈ On x ∈ R1 ⁡ y → A ∈ R1 ⁡ suc ⁡ suc ⁡ ⋃ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v A
6 fveq2 ⊢ y = suc ⁡ suc ⁡ ⋃ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v A → R1 ⁡ y = R1 ⁡ suc ⁡ suc ⁡ ⋃ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v A
7 6 eleq2d ⊢ y = suc ⁡ suc ⁡ ⋃ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v A → A ∈ R1 ⁡ y ↔ A ∈ R1 ⁡ suc ⁡ suc ⁡ ⋃ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v A
8 7 rspcev ⊢ suc ⁡ suc ⁡ ⋃ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v A ∈ On ∧ A ∈ R1 ⁡ suc ⁡ suc ⁡ ⋃ z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v A → ∃ y ∈ On A ∈ R1 ⁡ y
9 4 5 8 sylancr ⊢ ∀ x ∈ A ∃ y ∈ On x ∈ R1 ⁡ y → ∃ y ∈ On A ∈ R1 ⁡ y