Theorem dfac12lem2 10223

Description: Lemma for dfac12 10228. (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 8405	. . . . . . . . . . . . 13 ⊢ 𝐺 Fn On
3		fnfun 6639	. . . . . . . . . . . . 13 ⊢ (𝐺 Fn On → Fun 𝐺)
4	2, 3	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun 𝐺
5		dfac12.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ On)
6		funimaexg 6626	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V)
7	4, 5, 6	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ 𝐶) ∈ V)
8		uniexg 7757	. . . . . . . . . . 11 ⊢ ((𝐺 “ 𝐶) ∈ V → ∪ (𝐺 “ 𝐶) ∈ V)
9		rnexg 7914	. . . . . . . . . . 11 ⊢ (∪ (𝐺 “ 𝐶) ∈ V → ran ∪ (𝐺 “ 𝐶) ∈ V)
10	7, 8, 9	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ∈ V)
11		dfac12.8	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
12		f1f 6778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧):(𝑅1‘𝑧)⟶On)
13		fssxp 6737	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)⟶On → (𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On))
14		ssv 3955	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅1‘𝑧) ⊆ V
15		xpss1 5670	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅1‘𝑧) ⊆ V → ((𝑅1‘𝑧) × On) ⊆ (V × On))
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅1‘𝑧) × On) ⊆ (V × On)
17		sstr 3939	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) ∧ ((𝑅1‘𝑧) × On) ⊆ (V × On)) → (𝐺‘𝑧) ⊆ (V × On))
18	16, 17	mpan2 704	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ⊆ (V × On))
19		fvex 6898	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺‘𝑧) ∈ V
20	19	elpw 4561	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑧) ∈ 𝒫 (V × On) ↔ (𝐺‘𝑧) ⊆ (V × On))
21	18, 20	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ∈ 𝒫 (V × On))
22	12, 13, 21	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧) ∈ 𝒫 (V × On))
23	22	ralimi 3100	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
24	11, 23	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
25		onss 7799	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ On → 𝐶 ⊆ On)
26	5, 25	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ⊆ On)
27	2	fndmi 6643	. . . . . . . . . . . . . . . 16 ⊢ dom 𝐺 = On
28	26, 27	sseqtrrdi 3972	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ⊆ dom 𝐺)
29		funimass4 6949	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐺 ∧ 𝐶 ⊆ dom 𝐺) → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On)))
30	4, 28, 29	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On)))
31	24, 30	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺 “ 𝐶) ⊆ 𝒫 (V × On))
32		sspwuni 5060	. . . . . . . . . . . . 13 ⊢ ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∪ (𝐺 “ 𝐶) ⊆ (V × On))
33	31, 32	sylib 221	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (𝐺 “ 𝐶) ⊆ (V × On))
34		rnss 5921	. . . . . . . . . . . 12 ⊢ (∪ (𝐺 “ 𝐶) ⊆ (V × On) → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
35	33, 34	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
36		rnxpss 6164	. . . . . . . . . . 11 ⊢ ran (V × On) ⊆ On
37	35, 36	sstrdi 3943	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ On)
38		ssonuni 7794	. . . . . . . . . 10 ⊢ (ran ∪ (𝐺 “ 𝐶) ∈ V → (ran ∪ (𝐺 “ 𝐶) ⊆ On → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On))
39	10, 37, 38	sylc 66	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
40		onsuc 7824	. . . . . . . . 9 ⊢ (∪ ran ∪ (𝐺 “ 𝐶) ∈ On → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
41	39, 40	syl 18	. . . . . . . 8 ⊢ (𝜑 → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
42	41	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
43		rankon 9803	. . . . . . 7 ⊢ (rank‘𝑦) ∈ On
44		omcl 8544	. . . . . . 7 ⊢ ((suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On ∧ (rank‘𝑦) ∈ On) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On)
45	42, 43, 44	sylancl 598	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On)
46		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑧 = suc (rank‘𝑦) → (𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦)))
47		f1eq1 6773	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦)) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On))
48	46, 47	syl 18	. . . . . . . . . 10 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On))
49		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑧 = suc (rank‘𝑦) → (𝑅1‘𝑧) = (𝑅1‘suc (rank‘𝑦)))
50		f1eq2 6774	. . . . . . . . . . 11 ⊢ ((𝑅1‘𝑧) = (𝑅1‘suc (rank‘𝑦)) → ((𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
51	49, 50	syl 18	. . . . . . . . . 10 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
52	48, 51	bitrd 282	. . . . . . . . 9 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
53	11	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
54		rankr1ai 9806	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → (rank‘𝑦) ∈ 𝐶)
55	54	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ 𝐶)
56		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 = ∪ 𝐶)
57	55, 56	eleqtrd 2863	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ ∪ 𝐶)
58		eloni 6372	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
59	5, 58	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord 𝐶)
60	59	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → Ord 𝐶)
61		ordsucuniel 7835	. . . . . . . . . . 11 ⊢ (Ord 𝐶 → ((rank‘𝑦) ∈ ∪ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
62	60, 61	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((rank‘𝑦) ∈ ∪ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
63	57, 62	mpbid 235	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc (rank‘𝑦) ∈ 𝐶)
64	52, 53, 63	rspcdva 3578	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
65		f1f 6778	. . . . . . . 8 ⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
66	64, 65	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
67		r1elwf 9804	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
68	67	ad2antlr 740	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
69		rankidb 9808	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
70	68, 69	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
71	66, 70	ffvelcdmd 7085	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On)
72		oacl 8543	. . . . . 6 ⊢ (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
73	45, 71, 72	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
74		dfac12.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On)
75		f1f 6778	. . . . . . . 8 ⊢ (𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
76	74, 75	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
77	76	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
78		imassrn 6197	. . . . . . . 8 ⊢ (𝐻 “ 𝑦) ⊆ ran 𝐻
79		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘∪ 𝐶) ∈ V
80	79	rnex 7922	. . . . . . . . . . . . . 14 ⊢ ran (𝐺‘∪ 𝐶) ∈ V
81		fveq2 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∪ 𝐶 → (𝐺‘𝑧) = (𝐺‘∪ 𝐶))
82		f1eq1 6773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑧) = (𝐺‘∪ 𝐶) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On))
83	81, 82	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On))
84		fveq2 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∪ 𝐶 → (𝑅1‘𝑧) = (𝑅1‘∪ 𝐶))
85		f1eq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅1‘𝑧) = (𝑅1‘∪ 𝐶) → ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
86	84, 85	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
87	83, 86	bitrd 282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
88	11	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
89	5	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ∈ On)
90		onuni 7802	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ On → ∪ 𝐶 ∈ On)
91		sucidg 6446	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝐶 ∈ On → ∪ 𝐶 ∈ suc ∪ 𝐶)
92	89, 90, 91	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ suc ∪ 𝐶)
93	59	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → Ord 𝐶)
94		orduniorsuc 7841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
95	93, 94	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
96	95	orcanai 1018	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶)
97	92, 96	eleqtrrd 2864	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐶)
98	87, 88, 97	rspcdva 3578	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)
99		f1f 6778	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On)
100		frn 6717	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On → ran (𝐺‘∪ 𝐶) ⊆ On)
101	98, 99, 100	3syl 19	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ⊆ On)
102		epweon 7789	. . . . . . . . . . . . . . 15 ⊢ E We On
103		wess 5637	. . . . . . . . . . . . . . 15 ⊢ (ran (𝐺‘∪ 𝐶) ⊆ On → ( E We On → E We ran (𝐺‘∪ 𝐶)))
104	101, 102, 103	mpisyl 22	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → E We ran (𝐺‘∪ 𝐶))
105		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ OrdIso( E , ran (𝐺‘∪ 𝐶)) = OrdIso( E , ran (𝐺‘∪ 𝐶))
106	105	oiiso 9531	. . . . . . . . . . . . . 14 ⊢ ((ran (𝐺‘∪ 𝐶) ∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → OrdIso( E , ran (𝐺‘∪ 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)))
107	80, 104, 106	sylancr 599	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → OrdIso( E , ran (𝐺‘∪ 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)))
108		isof1o 7331	. . . . . . . . . . . . 13 ⊢ (OrdIso( E , ran (𝐺‘∪ 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)) → OrdIso( E , ran (𝐺‘∪ 𝐶)):dom OrdIso( E , ran (𝐺‘∪ 𝐶))–1-1-onto→ran (𝐺‘∪ 𝐶))
109		f1ocnv 6837	. . . . . . . . . . . . 13 ⊢ (OrdIso( E , ran (𝐺‘∪ 𝐶)):dom OrdIso( E , ran (𝐺‘∪ 𝐶))–1-1-onto→ran (𝐺‘∪ 𝐶) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
110		f1of1 6823	. . . . . . . . . . . . 13 ⊢ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1-onto→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
111	107, 108, 109, 110	4syl 20	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
112		f1f1orn 6836	. . . . . . . . . . . . 13 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶))
113		f1of1 6823	. . . . . . . . . . . . 13 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶))
114	98, 112, 113	3syl 19	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶))
115		f1co 6791	. . . . . . . . . . . 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 (𝐺‘∪ 𝐶)))
116	111, 114, 115	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
117		dfac12.h	. . . . . . . . . . . 12 ⊢ 𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶))
118		f1eq1 6773	. . . . . . . . . . . 12 ⊢ (𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)) → (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ↔ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶))))
119	117, 118	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ↔ (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
120	116, 119	sylibr 237	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
121		f1f 6778	. . . . . . . . . 10 ⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → 𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
122		frn 6717	. . . . . . . . . 10 ⊢ (𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
123	120, 121, 122	3syl 19	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
124		harcl 9553	. . . . . . . . . . 11 ⊢ (har‘(𝑅1‘𝐴)) ∈ On
125	124	onordi 6476	. . . . . . . . . 10 ⊢ Ord (har‘(𝑅1‘𝐴))
126	105	oion 9530	. . . . . . . . . . . 12 ⊢ (ran (𝐺‘∪ 𝐶) ∈ V → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
127	80, 126	mp1i 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
128	105	oien 9532	. . . . . . . . . . . . 13 ⊢ ((ran (𝐺‘∪ 𝐶) ∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶))
129	80, 104, 128	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶))
130		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ (𝑅1‘∪ 𝐶) ∈ V
131	130	f1oen 8999	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶) → (𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶))
132		ensym 9030	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶))
133	98, 112, 131, 132	4syl 20	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶))
134		fvex 6898	. . . . . . . . . . . . . 14 ⊢ (𝑅1‘𝐴) ∈ V
135		dfac12.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ On)
136	135	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐴 ∈ On)
137		dfac12.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
138	137	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ 𝐴)
139	138, 97	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐴)
140		r1ord2 9788	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → (∪ 𝐶 ∈ 𝐴 → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴)))
141	136, 139, 140	sylc 66	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴))
142		ssdomg 9027	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘𝐴) ∈ V → ((𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)))
143	134, 141, 142	mpsyl 69	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴))
144		endomtr 9039	. . . . . . . . . . . . 13 ⊢ ((ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶) ∧ (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
145	133, 143, 144	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
146		endomtr 9039	. . . . . . . . . . . 12 ⊢ ((dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶) ∧ ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼ (𝑅1‘𝐴))
147	129, 145, 146	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼ (𝑅1‘𝐴))
148		elharval 9555	. . . . . . . . . . 11 ⊢ (dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ (har‘(𝑅1‘𝐴)) ↔ (dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼ (𝑅1‘𝐴)))
149	127, 147, 148	sylanbrc 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ (har‘(𝑅1‘𝐴)))
150		ordelss 6378	. . . . . . . . . 10 ⊢ ((Ord (har‘(𝑅1‘𝐴)) ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ (har‘(𝑅1‘𝐴))) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ⊆ (har‘(𝑅1‘𝐴)))
151	125, 149, 150	sylancr 599	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ⊆ (har‘(𝑅1‘𝐴)))
152	123, 151	sstrd 3941	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ (har‘(𝑅1‘𝐴)))
153	78, 152	sstrid 3942	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
154		fvex 6898	. . . . . . . 8 ⊢ (har‘(𝑅1‘𝐴)) ∈ V
155	154	elpw2 5296	. . . . . . 7 ⊢ ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
156	153, 155	sylibr 237	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
157	77, 156	ffvelcdmd 7085	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐹‘(𝐻 “ 𝑦)) ∈ On)
158	73, 157	ifclda 4518	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On)
159	158	ex 418	. . 3 ⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On))
160		iftrue 4488	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)))
161		iftrue 4488	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)))
162	160, 161	eqeq12d 2777	. . . . . . 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‘𝑧))‘𝑧))))
163	162	adantl 487	. . . . . 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‘𝑧))‘𝑧))))
164	41	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
165		nsuceq0 6448	. . . . . . . 8 ⊢ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅
166	165	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅)
167	43	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ On)
168		onsucuni 7839	. . . . . . . . . . 11 ⊢ (ran ∪ (𝐺 “ 𝐶) ⊆ On → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
169	37, 168	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
170	169	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
171	26	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ On)
172		fnfvima 7239	. . . . . . . . . . . 12 ⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
173	2, 171, 63, 172	mp3an2i 1495	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
174		elssuni 4899	. . . . . . . . . . 11 ⊢ ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺 “ 𝐶))
175		rnss 5921	. . . . . . . . . . 11 ⊢ ((𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺 “ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪ (𝐺 “ 𝐶))
176	173, 174, 175	3syl 19	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪ (𝐺 “ 𝐶))
177		f1fn 6779	. . . . . . . . . . . 12 ⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
178	64, 177	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
179		fnfvelrn 7080	. . . . . . . . . . 11 ⊢ (((𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)) ∧ 𝑦 ∈ (𝑅1‘suc (rank‘𝑦))) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
180	178, 70, 179	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
181	176, 180	sseldd 3932	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran ∪ (𝐺 “ 𝐶))
182	170, 181	sseldd 3932	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
183	182	adantlrr 734	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
184		rankon 9803	. . . . . . . 8 ⊢ (rank‘𝑧) ∈ On
185	184	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑧) ∈ On)
186		eleq1w 2844	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1‘𝐶) ↔ 𝑧 ∈ (𝑅1‘𝐶)))
187	186	anbi2d 642	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ↔ (𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶))))
188	187	anbi1d 643	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶)))
189		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧))
190		suceq 6431	. . . . . . . . . . . . . 14 ⊢ ((rank‘𝑦) = (rank‘𝑧) → suc (rank‘𝑦) = suc (rank‘𝑧))
191	189, 190	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧))
192	191	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
193		id 23	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
194	192, 193	fveq12d 6892	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
195	194	eleq1d 2846	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶) ↔ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶)))
196	188, 195	imbi12d 347	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶)) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))))
197	196, 182	chvarvv 2022	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
198	197	adantlrl 733	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
199		omopth2 8592	. . . . . . 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‘𝑧))‘𝑧))))
200	164, 166, 167, 183, 185, 198, 199	syl222anc 1413	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))))
201	190	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧))
202	201	fveq2d 6889	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
203	202	fveq1d 6887	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
204	203	eqeq2d 2772	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
205	64	adantlrr 734	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
206	205	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
207	70	adantlrr 734	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
208	207	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
209		r1elwf 9804	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑅1‘𝐶) → 𝑧 ∈ ∪ (𝑅1 “ On))
210		rankidb 9808	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
211	209, 210	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑅1‘𝐶) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
212	211	ad2antll 742	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
213	212	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
214	201	fveq2d 6889	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc (rank‘𝑧)))
215	213, 214	eleqtrrd 2864	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))
216		f1fveq 7266	. . . . . . . . . . 11 ⊢ (((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On ∧ (𝑦 ∈ (𝑅1‘suc (rank‘𝑦)) ∧ 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
217	206, 208, 215, 216	syl12anc 850	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
218	204, 217	bitr3d 284	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧))
219	218	biimpd 232	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧))
220	219	expimpd 459	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧))
221	189, 194	jca 521	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
222	220, 221	impbid1 228	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧))
223	163, 200, 222	3bitrd 308	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
224		iffalse 4491	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = (𝐹‘(𝐻 “ 𝑦)))
225		iffalse 4491	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = (𝐹‘(𝐻 “ 𝑧)))
226	224, 225	eqeq12d 2777	. . . . . . 7 ⊢ (¬ 𝐶 = ∪ 𝐶 → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧))))
227	226	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧))))
228	74	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On)
229	156	adantlrr 734	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
230	187	anbi1d 643	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶)))
231		imaeq2 6048	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝐻 “ 𝑦) = (𝐻 “ 𝑧))
232	231	eleq1d 2846	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴))))
233	230, 232	imbi12d 347	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴))) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))))
234	233, 156	chvarvv 2022	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
235	234	adantlrl 733	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
236		f1fveq 7266	. . . . . . 7 ⊢ ((𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On ∧ ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ∧ (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧)))
237	228, 229, 235, 236	syl12anc 850	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧)))
238	120	adantlrr 734	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
239		simplrl 789	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘𝐶))
240	96	fveq2d 6889	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = (𝑅1‘suc ∪ 𝐶))
241		r1suc 9777	. . . . . . . . . . . 12 ⊢ (∪ 𝐶 ∈ On → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
242	89, 90, 241	3syl 19	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
243	240, 242	eqtrd 2796	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
244	243	adantlrr 734	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
245	239, 244	eleqtrd 2863	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ∈ 𝒫 (𝑅1‘∪ 𝐶))
246	245	elpwid 4566	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ⊆ (𝑅1‘∪ 𝐶))
247		simplrr 790	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ (𝑅1‘𝐶))
248	247, 244	eleqtrd 2863	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ 𝒫 (𝑅1‘∪ 𝐶))
249	248	elpwid 4566	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ⊆ (𝑅1‘∪ 𝐶))
250		f1imaeq 7269	. . . . . . 7 ⊢ ((𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∧ (𝑦 ⊆ (𝑅1‘∪ 𝐶) ∧ 𝑧 ⊆ (𝑅1‘∪ 𝐶))) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧))
251	238, 246, 249, 250	syl12anc 850	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧))
252	227, 237, 251	3bitrd 308	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
253	223, 252	pm2.61dan 825	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
254	253	ex 418	. . 3 ⊢ (𝜑 → ((𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶)) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)))
255	159, 254	dom2lem 9019	. 2 ⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On)
256	135, 74, 1, 5, 117	dfac12lem1 10222	. . 3 ⊢ (𝜑 → (𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))))
257		f1eq1 6773	. . 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))
258	256, 257	syl 18	. 2 ⊢ (𝜑 → ((𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On))
259	255, 258	mpbird 260	1 ⊢ (𝜑 → (𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  Vcvv 3451   ⊆ wss 3899  ∅c0 4279  ifcif 4482  𝒫 cpw 4557  ∪ cuni 4867   class class class wbr 5103   ↦ cmpt 5186   E cep 5550   We wwe 5603   × cxp 5649  ^◡ccnv 5650  dom cdm 5651  ran crn 5652   “ cima 5654   ∘ ccom 5655  Ord word 6361  Oncon0 6362  suc csuc 6364  Fun wfun 6532   Fn wfn 6533  ⟶wf 6534  –1-1→wf1 6535  –1-1-onto→wf1o 6537  ‘cfv 6538   Isom wiso 6539  (class class class)co 7420  recscrecs 8378   +_o coa 8473   ·_o comu 8474   ≈ cen 8970   ≼ cdom 8971  OrdIsocoi 9503  harchar 9550  𝑅₁cr1 9766  rankcrnk 9767

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-oadd 8480  df-omul 8481  df-er 8717  df-en 8974  df-dom 8975  df-oi 9504  df-har 9551  df-r1 9768  df-rank 9769

This theorem is used by:  dfac12lem3  10224