This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ V
Assertion tz9.13 ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 )

Proof

Step Hyp Ref Expression
1 tz9.13.1 ⊢ 𝐴 ∈ V
2 setind ⊢ ( ∀ 𝑧 ( 𝑧 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } → 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } ) → { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } = V )
3 ssel ⊢ ( 𝑧 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } ) )
4 vex ⊢ 𝑤 ∈ V
5 eleq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ 𝑤 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
6 5 rexbidv ⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝑤 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
7 4 6 elab ⊢ ( 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } ↔ ∃ 𝑥 ∈ On 𝑤 ∈ ( 𝑅1 ‘ 𝑥 ) )
8 3 7 imbitrdi ⊢ ( 𝑧 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } → ( 𝑤 ∈ 𝑧 → ∃ 𝑥 ∈ On 𝑤 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
9 8 ralrimiv ⊢ ( 𝑧 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } → ∀ 𝑤 ∈ 𝑧 ∃ 𝑥 ∈ On 𝑤 ∈ ( 𝑅1 ‘ 𝑥 ) )
10 vex ⊢ 𝑧 ∈ V
11 10 tz9.12 ⊢ ( ∀ 𝑤 ∈ 𝑧 ∃ 𝑥 ∈ On 𝑤 ∈ ( 𝑅1 ‘ 𝑥 ) → ∃ 𝑥 ∈ On 𝑧 ∈ ( 𝑅1 ‘ 𝑥 ) )
12 9 11 syl ⊢ ( 𝑧 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } → ∃ 𝑥 ∈ On 𝑧 ∈ ( 𝑅1 ‘ 𝑥 ) )
13 eleq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ 𝑧 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
14 13 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝑧 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
15 10 14 elab ⊢ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } ↔ ∃ 𝑥 ∈ On 𝑧 ∈ ( 𝑅1 ‘ 𝑥 ) )
16 12 15 sylibr ⊢ ( 𝑧 ⊆ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } → 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } )
17 2 16 mpg ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } = V
18 1 17 eleqtrri ⊢ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) }
19 eleq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
20 19 rexbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
21 1 20 elab ⊢ ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) } ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) )
22 18 21 mpbi ⊢ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 )