Theorem rankr1ai

Description: One direction of rankr1a . (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	rankr1ai	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ dom 𝑅1 )
2		r1val1	⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 𝒫 ( 𝑅1 ‘ 𝑥 ) )
3	2	eleq2d	⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
4		eliun	⊢ ( 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝒫 ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐵 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) )
5	3 4	syl6bb	⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
6		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
7	6	simpri	⊢ Lim dom 𝑅1
8		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
9	7 8	ax-mp	⊢ Ord dom 𝑅1
10		ordtr1	⊢ ( Ord dom 𝑅1 → ( ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 ) )
11	9 10	ax-mp	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 )
12	11	ancoms	⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ dom 𝑅1 )
13		r1sucg	⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
14	13	eleq2d	⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
15	12 14	syl	⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
16		ordsson	⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
17	9 16	ax-mp	⊢ dom 𝑅1 ⊆ On
18	17 12	sseldi	⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
19		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ↔ ( 𝑥 ∈ On ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
20		intss1	⊢ ( 𝑥 ∈ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 )
21	19 20	sylbir	⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 )
22	18 21	sylan	⊢ ( ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 )
23	22	ex	⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
24	15 23	sylbird	⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
25	24	reximdva	⊢ ( 𝐵 ∈ dom 𝑅1 → ( ∃ 𝑥 ∈ 𝐵 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) → ∃ 𝑥 ∈ 𝐵 ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
26	5 25	sylbid	⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
27	1 26	mpcom	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 )
28		r1elwf	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
29		rankvalb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
30	28 29	syl	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
31	30	sseq1d	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
32	31	adantr	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
33		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
34	17 1	sseldi	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ On )
35		ontr2	⊢ ( ( ( rank ‘ 𝐴 ) ∈ On ∧ 𝐵 ∈ On ) → ( ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
36	33 34 35	sylancr	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
37	36	expcomd	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝑥 ∈ 𝐵 → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) ) )
38	37	imp	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
39	32 38	sylbird	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
40	39	rexlimdva	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
41	27 40	mpd	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )