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𝑦 ) )