Theorem aomclem4

Description: Lemma for dfac11 . Limit case. Patch together well-orderings constructed so far using fnwe2 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Hypotheses	aomclem4.f	⊢ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) }
	aomclem4.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
	aomclem4.su	⊢ ( 𝜑 → dom 𝑧 = ∪ dom 𝑧 )
	aomclem4.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
Assertion	aomclem4	⊢ ( 𝜑 → 𝐹 We ( 𝑅1 ‘ dom 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		aomclem4.f	⊢ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) }
2		aomclem4.on	⊢ ( 𝜑 → dom 𝑧 ∈ On )
3		aomclem4.su	⊢ ( 𝜑 → dom 𝑧 = ∪ dom 𝑧 )
4		aomclem4.we	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
5		suceq	⊢ ( 𝑐 = ( rank ‘ 𝑎 ) → suc 𝑐 = suc ( rank ‘ 𝑎 ) )
6	5	fveq2d	⊢ ( 𝑐 = ( rank ‘ 𝑎 ) → ( 𝑧 ‘ suc 𝑐 ) = ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) )
7		r1fnon	⊢ 𝑅1 Fn On
8		fnfun	⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
9	7 8	ax-mp	⊢ Fun 𝑅1
10	7	fndmi	⊢ dom 𝑅1 = On
11	10	eqimss2i	⊢ On ⊆ dom 𝑅1
12	9 11	pm3.2i	⊢ ( Fun 𝑅1 ∧ On ⊆ dom 𝑅1 )
13		funfvima2	⊢ ( ( Fun 𝑅1 ∧ On ⊆ dom 𝑅1 ) → ( dom 𝑧 ∈ On → ( 𝑅1 ‘ dom 𝑧 ) ∈ ( 𝑅1 “ On ) ) )
14	12 2 13	mpsyl	⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) ∈ ( 𝑅1 “ On ) )
15		elssuni	⊢ ( ( 𝑅1 ‘ dom 𝑧 ) ∈ ( 𝑅1 “ On ) → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ∪ ( 𝑅1 “ On ) )
16	14 15	syl	⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ∪ ( 𝑅1 “ On ) )
17	16	sselda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → 𝑏 ∈ ∪ ( 𝑅1 “ On ) )
18		rankidb	⊢ ( 𝑏 ∈ ∪ ( 𝑅1 “ On ) → 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑏 ) ) )
19	17 18	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑏 ) ) )
20		suceq	⊢ ( ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) → suc ( rank ‘ 𝑏 ) = suc ( rank ‘ 𝑎 ) )
21	20	fveq2d	⊢ ( ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑏 ) ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
22	21	eleq2d	⊢ ( ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) → ( 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑏 ) ) ↔ 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) ) )
23	19 22	syl5ibcom	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) → 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) ) )
24	23	expimpd	⊢ ( 𝜑 → ( ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∧ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) ) → 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) ) )
25	24	ss2abdv	⊢ ( 𝜑 → { 𝑏 ∣ ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∧ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) ) } ⊆ { 𝑏 ∣ 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) } )
26		df-rab	⊢ { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } = { 𝑏 ∣ ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∧ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) ) }
27		abid1	⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) = { 𝑏 ∣ 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) }
28	25 26 27	3sstr4g	⊢ ( 𝜑 → { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
30		fveq2	⊢ ( 𝑏 = suc ( rank ‘ 𝑎 ) → ( 𝑧 ‘ 𝑏 ) = ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) )
31		fveq2	⊢ ( 𝑏 = suc ( rank ‘ 𝑎 ) → ( 𝑅1 ‘ 𝑏 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
32	30 31	weeq12d	⊢ ( 𝑏 = suc ( rank ‘ 𝑎 ) → ( ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) ↔ ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) ) )
33		fveq2	⊢ ( 𝑎 = 𝑏 → ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑏 ) )
34		fveq2	⊢ ( 𝑎 = 𝑏 → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ 𝑏 ) )
35	33 34	weeq12d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ↔ ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) ) )
36	35	cbvralvw	⊢ ( ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ↔ ∀ 𝑏 ∈ dom 𝑧 ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) )
37	4 36	sylib	⊢ ( 𝜑 → ∀ 𝑏 ∈ dom 𝑧 ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ∀ 𝑏 ∈ dom 𝑧 ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) )
39		rankr1ai	⊢ ( 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) → ( rank ‘ 𝑎 ) ∈ dom 𝑧 )
40	39	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( rank ‘ 𝑎 ) ∈ dom 𝑧 )
41		eloni	⊢ ( dom 𝑧 ∈ On → Ord dom 𝑧 )
42	2 41	syl	⊢ ( 𝜑 → Ord dom 𝑧 )
43		limsuc2	⊢ ( ( Ord dom 𝑧 ∧ dom 𝑧 = ∪ dom 𝑧 ) → ( ( rank ‘ 𝑎 ) ∈ dom 𝑧 ↔ suc ( rank ‘ 𝑎 ) ∈ dom 𝑧 ) )
44	42 3 43	syl2anc	⊢ ( 𝜑 → ( ( rank ‘ 𝑎 ) ∈ dom 𝑧 ↔ suc ( rank ‘ 𝑎 ) ∈ dom 𝑧 ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( ( rank ‘ 𝑎 ) ∈ dom 𝑧 ↔ suc ( rank ‘ 𝑎 ) ∈ dom 𝑧 ) )
46	40 45	mpbid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → suc ( rank ‘ 𝑎 ) ∈ dom 𝑧 )
47	32 38 46	rspcdva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
48		wess	⊢ ( { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) → ( ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) → ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } ) )
49	29 47 48	sylc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } )
50		rankf	⊢ rank : ∪ ( 𝑅1 “ On ) ⟶ On
51	50	a1i	⊢ ( 𝜑 → rank : ∪ ( 𝑅1 “ On ) ⟶ On )
52	51 16	fssresd	⊢ ( 𝜑 → ( rank ↾ ( 𝑅1 ‘ dom 𝑧 ) ) : ( 𝑅1 ‘ dom 𝑧 ) ⟶ On )
53		epweon	⊢ E We On
54	53	a1i	⊢ ( 𝜑 → E We On )
55	6 1 49 52 54	fnwe2	⊢ ( 𝜑 → 𝐹 We ( 𝑅1 ‘ dom 𝑧 ) )