Theorem rankwflemb

Description: Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	rankwflemb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		eluni	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) )
2		eleq2	⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ∈ 𝑦 ) )
3	2	biimprcd	⊢ ( 𝐴 ∈ 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
4		r1tr	⊢ Tr ( 𝑅1 ‘ 𝑥 )
5		trss	⊢ ( Tr ( 𝑅1 ‘ 𝑥 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
6	4 5	ax-mp	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) )
7		elpwg	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
8	6 7	mpbird	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) )
9		elfvdm	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝑥 ∈ dom 𝑅1 )
10		r1sucg	⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
11	9 10	syl	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
12	8 11	eleqtrrd	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
13	12	a1i	⊢ ( 𝑥 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
14	3 13	syl9	⊢ ( 𝐴 ∈ 𝑦 → ( 𝑥 ∈ On → ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) ) )
15	14	reximdvai	⊢ ( 𝐴 ∈ 𝑦 → ( ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
16		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
17	16	simpli	⊢ Fun 𝑅1
18		fvelima	⊢ ( ( Fun 𝑅1 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
19	17 18	mpan	⊢ ( 𝑦 ∈ ( 𝑅1 “ On ) → ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
20	15 19	impel	⊢ ( ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
21	20	exlimiv	⊢ ( ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
22	1 21	sylbi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
23		elfvdm	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → suc 𝑥 ∈ dom 𝑅1 )
24		fvelrn	⊢ ( ( Fun 𝑅1 ∧ suc 𝑥 ∈ dom 𝑅1 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ran 𝑅1 )
25	17 23 24	sylancr	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ran 𝑅1 )
26		df-ima	⊢ ( 𝑅1 “ On ) = ran ( 𝑅1 ↾ On )
27		funrel	⊢ ( Fun 𝑅1 → Rel 𝑅1 )
28	17 27	ax-mp	⊢ Rel 𝑅1
29	16	simpri	⊢ Lim dom 𝑅1
30		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
31		ordsson	⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
32	29 30 31	mp2b	⊢ dom 𝑅1 ⊆ On
33		relssres	⊢ ( ( Rel 𝑅1 ∧ dom 𝑅1 ⊆ On ) → ( 𝑅1 ↾ On ) = 𝑅1 )
34	28 32 33	mp2an	⊢ ( 𝑅1 ↾ On ) = 𝑅1
35	34	rneqi	⊢ ran ( 𝑅1 ↾ On ) = ran 𝑅1
36	26 35	eqtri	⊢ ( 𝑅1 “ On ) = ran 𝑅1
37	25 36	eleqtrrdi	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ( 𝑅1 “ On ) )
38		elunii	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ∧ ( 𝑅1 ‘ suc 𝑥 ) ∈ ( 𝑅1 “ On ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
39	37 38	mpdan	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
40	39	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
41	22 40	impbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )