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

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

Proof

Step Hyp Ref Expression
1 tz9.12.1 ⊢ 𝐴 ∈ V
2 eqid ⊢ ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) = ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } )
3 1 2 tz9.12lem2 ⊢ suc ∪ ( ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) “ 𝐴 ) ∈ On
4 3 onsuci ⊢ suc suc ∪ ( ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) “ 𝐴 ) ∈ On
5 1 2 tz9.12lem3 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝐴 ∈ ( 𝑅1 ‘ suc suc ∪ ( ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) “ 𝐴 ) ) )
6 fveq2 ⊢ ( 𝑦 = suc suc ∪ ( ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) “ 𝐴 ) → ( 𝑅1 ‘ 𝑦 ) = ( 𝑅1 ‘ suc suc ∪ ( ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) “ 𝐴 ) ) )
7 6 eleq2d ⊢ ( 𝑦 = suc suc ∪ ( ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) “ 𝐴 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc suc ∪ ( ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) “ 𝐴 ) ) ) )
8 7 rspcev ⊢ ( ( suc suc ∪ ( ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) “ 𝐴 ) ∈ On ∧ 𝐴 ∈ ( 𝑅1 ‘ suc suc ∪ ( ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ) “ 𝐴 ) ) ) → ∃ 𝑦 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) )
9 4 5 8 sylancr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ On 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → ∃ 𝑦 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) )