Theorem rankwflembOLD

Description: Obsolete version of rankwflemb as of 29-Sep-2026. (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	rankwflembOLD	⊢ ( 𝐴 ∈ ∪ ( 𝑅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		r1fun	⊢ Fun 𝑅1
17		fvelima	⊢ ( ( Fun 𝑅1 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
18	16 17	mpan	⊢ ( 𝑦 ∈ ( 𝑅1 “ On ) → ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
19	15 18	impel	⊢ ( ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
20	19	exlimiv	⊢ ( ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
21	1 20	sylbi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
22		elfvdm	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → suc 𝑥 ∈ dom 𝑅1 )
23		fvelrn	⊢ ( ( Fun 𝑅1 ∧ suc 𝑥 ∈ dom 𝑅1 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ran 𝑅1 )
24	16 22 23	sylancr	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ran 𝑅1 )
25		df-ima	⊢ ( 𝑅1 “ On ) = ran ( 𝑅1 ↾ On )
26		funrel	⊢ ( Fun 𝑅1 → Rel 𝑅1 )
27	16 26	ax-mp	⊢ Rel 𝑅1
28		r1dmlim	⊢ Lim dom 𝑅1
29		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
30		ordsson	⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
31	28 29 30	mp2b	⊢ dom 𝑅1 ⊆ On
32		relssres	⊢ ( ( Rel 𝑅1 ∧ dom 𝑅1 ⊆ On ) → ( 𝑅1 ↾ On ) = 𝑅1 )
33	27 31 32	mp2an	⊢ ( 𝑅1 ↾ On ) = 𝑅1
34	33	rneqi	⊢ ran ( 𝑅1 ↾ On ) = ran 𝑅1
35	25 34	eqtri	⊢ ( 𝑅1 “ On ) = ran 𝑅1
36	24 35	eleqtrrdi	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ( 𝑅1 “ On ) )
37		elunii	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ∧ ( 𝑅1 ‘ suc 𝑥 ) ∈ ( 𝑅1 “ On ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
38	36 37	mpdan	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
39	38	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
40	21 39	impbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )