Theorem dfac12lem2 9570

Description: Lemma for dfac12 9575. (Contributed by Mario Carneiro, 29-May-2015.)

Hypotheses

Ref	Expression
dfac12.1	⊢ (𝜑 → 𝐴 ∈ On)
dfac12.3	⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On)
dfac12.4	⊢ 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦))))))
dfac12.5	⊢ (𝜑 → 𝐶 ∈ On)
dfac12.h	⊢ 𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶))
dfac12.6	⊢ (𝜑 → 𝐶 ⊆ 𝐴)
dfac12.8	⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)

Assertion

Ref	Expression
dfac12lem2	⊢ (𝜑 → (𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On)

Distinct variable groups:   𝑦,𝑧,𝐴   𝑥,𝑦,𝑧,𝐶   𝑥,𝐺,𝑦,𝑧   𝜑,𝑦,𝑧   𝑥,𝐹,𝑦,𝑧   𝑦,𝐻,𝑧

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝐻(𝑥)

Proof of Theorem dfac12lem2

Step	Hyp	Ref	Expression
1		dfac12.4	. . . . . . . . . . . . . 14 ⊢ 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦))))))
2	1	tfr1 8033	. . . . . . . . . . . . 13 ⊢ 𝐺 Fn On
3		fnfun 6453	. . . . . . . . . . . . 13 ⊢ (𝐺 Fn On → Fun 𝐺)
4	2, 3	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun 𝐺
5		dfac12.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ On)
6		funimaexg 6440	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V)
7	4, 5, 6	sylancr 589	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ 𝐶) ∈ V)
8		uniexg 7466	. . . . . . . . . . 11 ⊢ ((𝐺 “ 𝐶) ∈ V → ∪ (𝐺 “ 𝐶) ∈ V)
9		rnexg 7614	. . . . . . . . . . 11 ⊢ (∪ (𝐺 “ 𝐶) ∈ V → ran ∪ (𝐺 “ 𝐶) ∈ V)
10	7, 8, 9	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ∈ V)
11		dfac12.8	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
12		f1f 6575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧):(𝑅1‘𝑧)⟶On)
13		fssxp 6534	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)⟶On → (𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On))
14		ssv 3991	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅1‘𝑧) ⊆ V
15		xpss1 5574	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅1‘𝑧) ⊆ V → ((𝑅1‘𝑧) × On) ⊆ (V × On))
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅1‘𝑧) × On) ⊆ (V × On)
17		sstr 3975	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) ∧ ((𝑅1‘𝑧) × On) ⊆ (V × On)) → (𝐺‘𝑧) ⊆ (V × On))
18	16, 17	mpan2 689	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ⊆ (V × On))
19		fvex 6683	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺‘𝑧) ∈ V
20	19	elpw 4543	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑧) ∈ 𝒫 (V × On) ↔ (𝐺‘𝑧) ⊆ (V × On))
21	18, 20	sylibr 236	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ∈ 𝒫 (V × On))
22	12, 13, 21	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧) ∈ 𝒫 (V × On))
23	22	ralimi 3160	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
24	11, 23	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
25		onss 7505	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ On → 𝐶 ⊆ On)
26	5, 25	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ⊆ On)
27		fndm 6455	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 Fn On → dom 𝐺 = On)
28	2, 27	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ dom 𝐺 = On
29	26, 28	sseqtrrdi 4018	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ⊆ dom 𝐺)
30		funimass4 6730	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐺 ∧ 𝐶 ⊆ dom 𝐺) → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On)))
31	4, 29, 30	sylancr 589	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On)))
32	24, 31	mpbird 259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺 “ 𝐶) ⊆ 𝒫 (V × On))
33		sspwuni 5022	. . . . . . . . . . . . 13 ⊢ ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∪ (𝐺 “ 𝐶) ⊆ (V × On))
34	32, 33	sylib 220	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (𝐺 “ 𝐶) ⊆ (V × On))
35		rnss 5809	. . . . . . . . . . . 12 ⊢ (∪ (𝐺 “ 𝐶) ⊆ (V × On) → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
36	34, 35	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
37		rnxpss 6029	. . . . . . . . . . 11 ⊢ ran (V × On) ⊆ On
38	36, 37	sstrdi 3979	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ On)
39		ssonuni 7501	. . . . . . . . . 10 ⊢ (ran ∪ (𝐺 “ 𝐶) ∈ V → (ran ∪ (𝐺 “ 𝐶) ⊆ On → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On))
40	10, 38, 39	sylc 65	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
41		suceloni 7528	. . . . . . . . 9 ⊢ (∪ ran ∪ (𝐺 “ 𝐶) ∈ On → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
42	40, 41	syl 17	. . . . . . . 8 ⊢ (𝜑 → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
43	42	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
44		rankon 9224	. . . . . . 7 ⊢ (rank‘𝑦) ∈ On
45		omcl 8161	. . . . . . 7 ⊢ ((suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On ∧ (rank‘𝑦) ∈ On) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On)
46	43, 44, 45	sylancl 588	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On)
47		fveq2 6670	. . . . . . . . . . 11 ⊢ (𝑧 = suc (rank‘𝑦) → (𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦)))
48		f1eq1 6570	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦)) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On))
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On))
50		fveq2 6670	. . . . . . . . . . 11 ⊢ (𝑧 = suc (rank‘𝑦) → (𝑅1‘𝑧) = (𝑅1‘suc (rank‘𝑦)))
51		f1eq2 6571	. . . . . . . . . . 11 ⊢ ((𝑅1‘𝑧) = (𝑅1‘suc (rank‘𝑦)) → ((𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
52	50, 51	syl 17	. . . . . . . . . 10 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
53	49, 52	bitrd 281	. . . . . . . . 9 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
54	11	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
55		rankr1ai 9227	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → (rank‘𝑦) ∈ 𝐶)
56	55	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ 𝐶)
57		simpr 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 = ∪ 𝐶)
58	56, 57	eleqtrd 2915	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ ∪ 𝐶)
59		eloni 6201	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
60	5, 59	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord 𝐶)
61	60	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → Ord 𝐶)
62		ordsucuniel 7539	. . . . . . . . . . 11 ⊢ (Ord 𝐶 → ((rank‘𝑦) ∈ ∪ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
63	61, 62	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((rank‘𝑦) ∈ ∪ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
64	58, 63	mpbid 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc (rank‘𝑦) ∈ 𝐶)
65	53, 54, 64	rspcdva 3625	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
66		f1f 6575	. . . . . . . 8 ⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
67	65, 66	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
68		r1elwf 9225	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
69	68	ad2antlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
70		rankidb 9229	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
71	69, 70	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
72	67, 71	ffvelrnd 6852	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On)
73		oacl 8160	. . . . . 6 ⊢ (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
74	46, 72, 73	syl2anc 586	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
75		dfac12.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On)
76		f1f 6575	. . . . . . . 8 ⊢ (𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
77	75, 76	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
78	77	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
79		imassrn 5940	. . . . . . . 8 ⊢ (𝐻 “ 𝑦) ⊆ ran 𝐻
80		fvex 6683	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘∪ 𝐶) ∈ V
81	80	rnex 7617	. . . . . . . . . . . . . 14 ⊢ ran (𝐺‘∪ 𝐶) ∈ V
82		fveq2 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∪ 𝐶 → (𝐺‘𝑧) = (𝐺‘∪ 𝐶))
83		f1eq1 6570	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑧) = (𝐺‘∪ 𝐶) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On))
84	82, 83	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On))
85		fveq2 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∪ 𝐶 → (𝑅1‘𝑧) = (𝑅1‘∪ 𝐶))
86		f1eq2 6571	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅1‘𝑧) = (𝑅1‘∪ 𝐶) → ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
87	85, 86	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
88	84, 87	bitrd 281	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
89	11	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
90	5	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ∈ On)
91		onuni 7508	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ On → ∪ 𝐶 ∈ On)
92		sucidg 6269	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝐶 ∈ On → ∪ 𝐶 ∈ suc ∪ 𝐶)
93	90, 91, 92	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ suc ∪ 𝐶)
94	60	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → Ord 𝐶)
95		orduniorsuc 7545	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
97	96	orcanai 999	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶)
98	93, 97	eleqtrrd 2916	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐶)
99	88, 89, 98	rspcdva 3625	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)
100		f1f 6575	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On)
101		frn 6520	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On → ran (𝐺‘∪ 𝐶) ⊆ On)
102	99, 100, 101	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ⊆ On)
103		epweon 7497	. . . . . . . . . . . . . . 15 ⊢ E We On
104		wess 5542	. . . . . . . . . . . . . . 15 ⊢ (ran (𝐺‘∪ 𝐶) ⊆ On → ( E We On → E We ran (𝐺‘∪ 𝐶)))
105	102, 103, 104	mpisyl 21	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → E We ran (𝐺‘∪ 𝐶))
106		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ OrdIso( E , ran (𝐺‘∪ 𝐶)) = OrdIso( E , ran (𝐺‘∪ 𝐶))
107	106	oiiso 9001	. . . . . . . . . . . . . 14 ⊢ ((ran (𝐺‘∪ 𝐶) ∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → OrdIso( E , ran (𝐺‘∪ 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)))
108	81, 105, 107	sylancr 589	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → OrdIso( E , ran (𝐺‘∪ 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)))
109		isof1o 7076	. . . . . . . . . . . . 13 ⊢ (OrdIso( E , ran (𝐺‘∪ 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)) → OrdIso( E , ran (𝐺‘∪ 𝐶)):dom OrdIso( E , ran (𝐺‘∪ 𝐶))–1-1-onto→ran (𝐺‘∪ 𝐶))
110		f1ocnv 6627	. . . . . . . . . . . . 13 ⊢ (OrdIso( E , ran (𝐺‘∪ 𝐶)):dom OrdIso( E , ran (𝐺‘∪ 𝐶))–1-1-onto→ran (𝐺‘∪ 𝐶) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
111		f1of1 6614	. . . . . . . . . . . . 13 ⊢ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
112	108, 109, 110, 111	4syl 19	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
113		f1f1orn 6626	. . . . . . . . . . . . 13 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶))
114		f1of1 6614	. . . . . . . . . . . . 13 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶))
115	99, 113, 114	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶))
116		f1co 6585	. . . . . . . . . . . 12 ⊢ ((◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∧ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶)) → (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
117	112, 115, 116	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
118		dfac12.h	. . . . . . . . . . . 12 ⊢ 𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶))
119		f1eq1 6570	. . . . . . . . . . . 12 ⊢ (𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)) → (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ↔ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))))
120	118, 119	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ↔ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
121	117, 120	sylibr 236	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
122		f1f 6575	. . . . . . . . . 10 ⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → 𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
123		frn 6520	. . . . . . . . . 10 ⊢ (𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
124	121, 122, 123	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
125		harcl 9025	. . . . . . . . . . 11 ⊢ (har‘(𝑅1‘𝐴)) ∈ On
126	125	onordi 6295	. . . . . . . . . 10 ⊢ Ord (har‘(𝑅1‘𝐴))
127	106	oion 9000	. . . . . . . . . . . 12 ⊢ (ran (𝐺‘∪ 𝐶) ∈ V → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
128	81, 127	mp1i 13	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
129	106	oien 9002	. . . . . . . . . . . . 13 ⊢ ((ran (𝐺‘∪ 𝐶) ∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶))
130	81, 105, 129	sylancr 589	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶))
131		fvex 6683	. . . . . . . . . . . . . . 15 ⊢ (𝑅1‘∪ 𝐶) ∈ V
132	131	f1oen 8530	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶) → (𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶))
133		ensym 8558	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶))
134	99, 113, 132, 133	4syl 19	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶))
135		fvex 6683	. . . . . . . . . . . . . 14 ⊢ (𝑅1‘𝐴) ∈ V
136		dfac12.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ On)
137	136	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐴 ∈ On)
138		dfac12.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
139	138	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ 𝐴)
140	139, 98	sseldd 3968	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐴)
141		r1ord2 9210	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → (∪ 𝐶 ∈ 𝐴 → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴)))
142	137, 140, 141	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴))
143		ssdomg 8555	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘𝐴) ∈ V → ((𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)))
144	135, 142, 143	mpsyl 68	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴))
145		endomtr 8567	. . . . . . . . . . . . 13 ⊢ ((ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶) ∧ (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
146	134, 144, 145	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
147		endomtr 8567	. . . . . . . . . . . 12 ⊢ ((dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶) ∧ ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼ (𝑅1‘𝐴))
148	130, 146, 147	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼ (𝑅1‘𝐴))
149		elharval 9027	. . . . . . . . . . 11 ⊢ (dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ (har‘(𝑅1‘𝐴)) ↔ (dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼ (𝑅1‘𝐴)))
150	128, 148, 149	sylanbrc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ (har‘(𝑅1‘𝐴)))
151		ordelss 6207	. . . . . . . . . 10 ⊢ ((Ord (har‘(𝑅1‘𝐴)) ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ (har‘(𝑅1‘𝐴))) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ⊆ (har‘(𝑅1‘𝐴)))
152	126, 150, 151	sylancr 589	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ⊆ (har‘(𝑅1‘𝐴)))
153	124, 152	sstrd 3977	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ (har‘(𝑅1‘𝐴)))
154	79, 153	sstrid 3978	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
155		fvex 6683	. . . . . . . 8 ⊢ (har‘(𝑅1‘𝐴)) ∈ V
156	155	elpw2 5248	. . . . . . 7 ⊢ ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
157	154, 156	sylibr 236	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
158	78, 157	ffvelrnd 6852	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐹‘(𝐻 “ 𝑦)) ∈ On)
159	74, 158	ifclda 4501	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On)
160	159	ex 415	. . 3 ⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On))
161		iftrue 4473	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)))
162		iftrue 4473	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)))
163	161, 162	eqeq12d 2837	. . . . . . 7 ⊢ (𝐶 = ∪ 𝐶 → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧))))
164	163	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧))))
165	42	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
166		nsuceq0 6271	. . . . . . . 8 ⊢ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅
167	166	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅)
168	44	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ On)
169		onsucuni 7543	. . . . . . . . . . 11 ⊢ (ran ∪ (𝐺 “ 𝐶) ⊆ On → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
170	38, 169	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
171	170	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
172	26	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ On)
173		fnfvima 6995	. . . . . . . . . . . 12 ⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
174	2, 172, 64, 173	mp3an2i 1462	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
175		elssuni 4868	. . . . . . . . . . 11 ⊢ ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺 “ 𝐶))
176		rnss 5809	. . . . . . . . . . 11 ⊢ ((𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺 “ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪ (𝐺 “ 𝐶))
177	174, 175, 176	3syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪ (𝐺 “ 𝐶))
178		f1fn 6576	. . . . . . . . . . . 12 ⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
179	65, 178	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
180		fnfvelrn 6848	. . . . . . . . . . 11 ⊢ (((𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)) ∧ 𝑦 ∈ (𝑅1‘suc (rank‘𝑦))) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
181	179, 71, 180	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
182	177, 181	sseldd 3968	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran ∪ (𝐺 “ 𝐶))
183	171, 182	sseldd 3968	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
184	183	adantlrr 719	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
185		rankon 9224	. . . . . . . 8 ⊢ (rank‘𝑧) ∈ On
186	185	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑧) ∈ On)
187		eleq1w 2895	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1‘𝐶) ↔ 𝑧 ∈ (𝑅1‘𝐶)))
188	187	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ↔ (𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶))))
189	188	anbi1d 631	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶)))
190		fveq2 6670	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧))
191		suceq 6256	. . . . . . . . . . . . . 14 ⊢ ((rank‘𝑦) = (rank‘𝑧) → suc (rank‘𝑦) = suc (rank‘𝑧))
192	190, 191	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧))
193	192	fveq2d 6674	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
194		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
195	193, 194	fveq12d 6677	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
196	195	eleq1d 2897	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶) ↔ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶)))
197	189, 196	imbi12d 347	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶)) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))))
198	197, 183	chvarvv 2005	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
199	198	adantlrl 718	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
200		omopth2 8210	. . . . . . 7 ⊢ (((suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On ∧ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅) ∧ ((rank‘𝑦) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶)) ∧ ((rank‘𝑧) ∈ On ∧ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))) → (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))))
201	165, 167, 168, 184, 186, 199, 200	syl222anc 1382	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))))
202	191	adantl 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧))
203	202	fveq2d 6674	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
204	203	fveq1d 6672	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
205	204	eqeq2d 2832	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
206	65	adantlrr 719	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
207	206	adantr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
208	71	adantlrr 719	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
209	208	adantr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
210		r1elwf 9225	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑅1‘𝐶) → 𝑧 ∈ ∪ (𝑅1 “ On))
211		rankidb 9229	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
212	210, 211	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑅1‘𝐶) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
213	212	ad2antll 727	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
214	213	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
215	202	fveq2d 6674	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc (rank‘𝑧)))
216	214, 215	eleqtrrd 2916	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))
217		f1fveq 7020	. . . . . . . . . . 11 ⊢ (((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On ∧ (𝑦 ∈ (𝑅1‘suc (rank‘𝑦)) ∧ 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
218	207, 209, 216, 217	syl12anc 834	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
219	205, 218	bitr3d 283	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧))
220	219	biimpd 231	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧))
221	220	expimpd 456	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧))
222	190, 195	jca 514	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
223	221, 222	impbid1 227	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧))
224	164, 201, 223	3bitrd 307	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
225		iffalse 4476	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = (𝐹‘(𝐻 “ 𝑦)))
226		iffalse 4476	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = (𝐹‘(𝐻 “ 𝑧)))
227	225, 226	eqeq12d 2837	. . . . . . 7 ⊢ (¬ 𝐶 = ∪ 𝐶 → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧))))
228	227	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧))))
229	75	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On)
230	157	adantlrr 719	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
231	188	anbi1d 631	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶)))
232		imaeq2 5925	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝐻 “ 𝑦) = (𝐻 “ 𝑧))
233	232	eleq1d 2897	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴))))
234	231, 233	imbi12d 347	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴))) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))))
235	234, 157	chvarvv 2005	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
236	235	adantlrl 718	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
237		f1fveq 7020	. . . . . . 7 ⊢ ((𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On ∧ ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ∧ (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧)))
238	229, 230, 236, 237	syl12anc 834	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧)))
239	121	adantlrr 719	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
240		simplrl 775	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘𝐶))
241	97	fveq2d 6674	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = (𝑅1‘suc ∪ 𝐶))
242		r1suc 9199	. . . . . . . . . . . 12 ⊢ (∪ 𝐶 ∈ On → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
243	90, 91, 242	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
244	241, 243	eqtrd 2856	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
245	244	adantlrr 719	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
246	240, 245	eleqtrd 2915	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ∈ 𝒫 (𝑅1‘∪ 𝐶))
247	246	elpwid 4550	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ⊆ (𝑅1‘∪ 𝐶))
248		simplrr 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ (𝑅1‘𝐶))
249	248, 245	eleqtrd 2915	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ 𝒫 (𝑅1‘∪ 𝐶))
250	249	elpwid 4550	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ⊆ (𝑅1‘∪ 𝐶))
251		f1imaeq 7023	. . . . . . 7 ⊢ ((𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∧ (𝑦 ⊆ (𝑅1‘∪ 𝐶) ∧ 𝑧 ⊆ (𝑅1‘∪ 𝐶))) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧))
252	239, 247, 250, 251	syl12anc 834	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧))
253	228, 238, 252	3bitrd 307	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
254	224, 253	pm2.61dan 811	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
255	254	ex 415	. . 3 ⊢ (𝜑 → ((𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶)) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)))
256	160, 255	dom2lem 8549	. 2 ⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On)
257	136, 75, 1, 5, 118	dfac12lem1 9569	. . 3 ⊢ (𝜑 → (𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))))
258		f1eq1 6570	. . 3 ⊢ ((𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))) → ((𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On))
259	257, 258	syl 17	. 2 ⊢ (𝜑 → ((𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On))
260	256, 259	mpbird 259	1 ⊢ (𝜑 → (𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1537   ∈ wcel 2114   ≠ wne 3016  ∀wral 3138  Vcvv 3494   ⊆ wss 3936  ∅c0 4291  ifcif 4467  𝒫 cpw 4539  ∪ cuni 4838   class class class wbr 5066   ↦ cmpt 5146   E cep 5464   We wwe 5513   × cxp 5553  ^◡ccnv 5554  dom cdm 5555  ran crn 5556   “ cima 5558   ∘ ccom 5559  Ord word 6190  Oncon0 6191  suc csuc 6193  Fun wfun 6349   Fn wfn 6350  ⟶wf 6351  –1-1→wf1 6352  –1-1-onto→wf1o 6354  ‘cfv 6355   Isom wiso 6356  (class class class)co 7156  recscrecs 8007   +_o coa 8099   ·_o comu 8100   ≈ cen 8506   ≼ cdom 8507  OrdIsocoi 8973  harchar 9020  𝑅₁cr1 9191  rankcrnk 9192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-se 5515  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-isom 6364  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-oadd 8106  df-omul 8107  df-er 8289  df-en 8510  df-dom 8511  df-oi 8974  df-har 9022  df-r1 9193  df-rank 9194

This theorem is referenced by:  dfac12lem3  9571