Metamath Proof Explorer

Theorem tz9.13

Description: Every set is well-founded, assuming the Axiom of Regularity. In other words, every set belongs to a layer of the cumulative hierarchy of sets. Proposition 9.13 of TakeutiZaring p. 78. (Contributed by NM, 23-Sep-2003)

Ref Expression
Hypothesis tz9.13.1 ⊢A∈V
Assertion tz9.13 ⊢∃x∈OnA∈R1⁡x

Proof

Step Hyp Ref Expression
1 tz9.13.1 ⊢A∈V
2 setind ⊢∀zz⊆y|∃x∈Ony∈R1⁡x→z∈y|∃x∈Ony∈R1⁡x→y|∃x∈Ony∈R1⁡x=V
3 ssel ⊢z⊆y|∃x∈Ony∈R1⁡x→w∈z→w∈y|∃x∈Ony∈R1⁡x
4 vex ⊢w∈V
5 eleq1 ⊢y=w→y∈R1⁡x↔w∈R1⁡x
6 5 rexbidv ⊢y=w→∃x∈Ony∈R1⁡x↔∃x∈Onw∈R1⁡x
7 4 6 elab ⊢w∈y|∃x∈Ony∈R1⁡x↔∃x∈Onw∈R1⁡x
8 3 7 imbitrdi ⊢z⊆y|∃x∈Ony∈R1⁡x→w∈z→∃x∈Onw∈R1⁡x
9 8 ralrimiv ⊢z⊆y|∃x∈Ony∈R1⁡x→∀w∈z∃x∈Onw∈R1⁡x
10 vex ⊢z∈V
11 10 tz9.12 ⊢∀w∈z∃x∈Onw∈R1⁡x→∃x∈Onz∈R1⁡x
12 9 11 syl ⊢z⊆y|∃x∈Ony∈R1⁡x→∃x∈Onz∈R1⁡x
13 eleq1 ⊢y=z→y∈R1⁡x↔z∈R1⁡x
14 13 rexbidv ⊢y=z→∃x∈Ony∈R1⁡x↔∃x∈Onz∈R1⁡x
15 10 14 elab ⊢z∈y|∃x∈Ony∈R1⁡x↔∃x∈Onz∈R1⁡x
16 12 15 sylibr ⊢z⊆y|∃x∈Ony∈R1⁡x→z∈y|∃x∈Ony∈R1⁡x
17 2 16 mpg ⊢y|∃x∈Ony∈R1⁡x=V
18 1 17 eleqtrri ⊢A∈y|∃x∈Ony∈R1⁡x
19 eleq1 ⊢y=A→y∈R1⁡x↔A∈R1⁡x
20 19 rexbidv ⊢y=A→∃x∈Ony∈R1⁡x↔∃x∈OnA∈R1⁡x
21 1 20 elab ⊢A∈y|∃x∈Ony∈R1⁡x↔∃x∈OnA∈R1⁡x
22 18 21 mpbi ⊢∃x∈OnA∈R1⁡x