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