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