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 stage 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 ∈ On A ∈ R1 ⁡ x

Proof

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