Theorem dfac12lem2 10182

Description: Lemma for dfac12 10187. (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 8435	. . . . . . . . . . . . 13 ⊢ 𝐺 Fn On
3		fnfun 6668	. . . . . . . . . . . . 13 ⊢ (𝐺 Fn On → Fun 𝐺)
4	2, 3	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun 𝐺
5		dfac12.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ On)
6		funimaexg 6653	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V)
7	4, 5, 6	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ 𝐶) ∈ V)
8		uniexg 7758	. . . . . . . . . . 11 ⊢ ((𝐺 “ 𝐶) ∈ V → ∪ (𝐺 “ 𝐶) ∈ V)
9		rnexg 7924	. . . . . . . . . . 11 ⊢ (∪ (𝐺 “ 𝐶) ∈ V → ran ∪ (𝐺 “ 𝐶) ∈ V)
10	7, 8, 9	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ∈ V)
11		dfac12.8	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
12		f1f 6804	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧):(𝑅1‘𝑧)⟶On)
13		fssxp 6763	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)⟶On → (𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On))
14		ssv 4019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅1‘𝑧) ⊆ V
15		xpss1 5707	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅1‘𝑧) ⊆ V → ((𝑅1‘𝑧) × On) ⊆ (V × On))
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅1‘𝑧) × On) ⊆ (V × On)
17		sstr 4003	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) ∧ ((𝑅1‘𝑧) × On) ⊆ (V × On)) → (𝐺‘𝑧) ⊆ (V × On))
18	16, 17	mpan2 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ⊆ (V × On))
19		fvex 6919	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺‘𝑧) ∈ V
20	19	elpw 4608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑧) ∈ 𝒫 (V × On) ↔ (𝐺‘𝑧) ⊆ (V × On))
21	18, 20	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ∈ 𝒫 (V × On))
22	12, 13, 21	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧) ∈ 𝒫 (V × On))
23	22	ralimi 3080	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
24	11, 23	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
25		onss 7803	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ On → 𝐶 ⊆ On)
26	5, 25	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ⊆ On)
27	2	fndmi 6672	. . . . . . . . . . . . . . . 16 ⊢ dom 𝐺 = On
28	26, 27	sseqtrrdi 4046	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ⊆ dom 𝐺)
29		funimass4 6972	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐺 ∧ 𝐶 ⊆ dom 𝐺) → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On)))
30	4, 28, 29	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On)))
31	24, 30	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺 “ 𝐶) ⊆ 𝒫 (V × On))
32		sspwuni 5104	. . . . . . . . . . . . 13 ⊢ ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∪ (𝐺 “ 𝐶) ⊆ (V × On))
33	31, 32	sylib 218	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (𝐺 “ 𝐶) ⊆ (V × On))
34		rnss 5952	. . . . . . . . . . . 12 ⊢ (∪ (𝐺 “ 𝐶) ⊆ (V × On) → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
35	33, 34	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
36		rnxpss 6193	. . . . . . . . . . 11 ⊢ ran (V × On) ⊆ On
37	35, 36	sstrdi 4007	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ On)
38		ssonuni 7798	. . . . . . . . . 10 ⊢ (ran ∪ (𝐺 “ 𝐶) ∈ V → (ran ∪ (𝐺 “ 𝐶) ⊆ On → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On))
39	10, 37, 38	sylc 65	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
40		onsuc 7830	. . . . . . . . 9 ⊢ (∪ ran ∪ (𝐺 “ 𝐶) ∈ On → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
41	39, 40	syl 17	. . . . . . . 8 ⊢ (𝜑 → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
42	41	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
43		rankon 9832	. . . . . . 7 ⊢ (rank‘𝑦) ∈ On
44		omcl 8572	. . . . . . 7 ⊢ ((suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On ∧ (rank‘𝑦) ∈ On) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On)
45	42, 43, 44	sylancl 586	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On)
46		fveq2 6906	. . . . . . . . . . 11 ⊢ (𝑧 = suc (rank‘𝑦) → (𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦)))
47		f1eq1 6799	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦)) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On))
48	46, 47	syl 17	. . . . . . . . . 10 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On))
49		fveq2 6906	. . . . . . . . . . 11 ⊢ (𝑧 = suc (rank‘𝑦) → (𝑅1‘𝑧) = (𝑅1‘suc (rank‘𝑦)))
50		f1eq2 6800	. . . . . . . . . . 11 ⊢ ((𝑅1‘𝑧) = (𝑅1‘suc (rank‘𝑦)) → ((𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
51	49, 50	syl 17	. . . . . . . . . 10 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘suc (rank‘𝑦)):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
52	48, 51	bitrd 279	. . . . . . . . 9 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
53	11	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
54		rankr1ai 9835	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → (rank‘𝑦) ∈ 𝐶)
55	54	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ 𝐶)
56		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 = ∪ 𝐶)
57	55, 56	eleqtrd 2840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ ∪ 𝐶)
58		eloni 6395	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
59	5, 58	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord 𝐶)
60	59	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → Ord 𝐶)
61		ordsucuniel 7843	. . . . . . . . . . 11 ⊢ (Ord 𝐶 → ((rank‘𝑦) ∈ ∪ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
62	60, 61	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((rank‘𝑦) ∈ ∪ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
63	57, 62	mpbid 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc (rank‘𝑦) ∈ 𝐶)
64	52, 53, 63	rspcdva 3622	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
65		f1f 6804	. . . . . . . 8 ⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
66	64, 65	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))⟶On)
67		r1elwf 9833	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
68	67	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
69		rankidb 9837	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
70	68, 69	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
71	66, 70	ffvelcdmd 7104	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On)
72		oacl 8571	. . . . . 6 ⊢ (((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) ∈ On ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
73	45, 71, 72	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)) ∈ On)
74		dfac12.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On)
75		f1f 6804	. . . . . . . 8 ⊢ (𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
76	74, 75	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
77	76	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
78		imassrn 6090	. . . . . . . 8 ⊢ (𝐻 “ 𝑦) ⊆ ran 𝐻
79		fvex 6919	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘∪ 𝐶) ∈ V
80	79	rnex 7932	. . . . . . . . . . . . . 14 ⊢ ran (𝐺‘∪ 𝐶) ∈ V
81		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∪ 𝐶 → (𝐺‘𝑧) = (𝐺‘∪ 𝐶))
82		f1eq1 6799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑧) = (𝐺‘∪ 𝐶) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On))
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On))
84		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∪ 𝐶 → (𝑅1‘𝑧) = (𝑅1‘∪ 𝐶))
85		f1eq2 6800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅1‘𝑧) = (𝑅1‘∪ 𝐶) → ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘∪ 𝐶):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
87	83, 86	bitrd 279	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
88	11	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
89	5	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ∈ On)
90		onuni 7807	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ On → ∪ 𝐶 ∈ On)
91		sucidg 6466	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝐶 ∈ On → ∪ 𝐶 ∈ suc ∪ 𝐶)
92	89, 90, 91	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ suc ∪ 𝐶)
93	59	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → Ord 𝐶)
94		orduniorsuc 7849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
95	93, 94	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
96	95	orcanai 1004	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶)
97	92, 96	eleqtrrd 2841	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐶)
98	87, 88, 97	rspcdva 3622	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)
99		f1f 6804	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On)
100		frn 6743	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On → ran (𝐺‘∪ 𝐶) ⊆ On)
101	98, 99, 100	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ⊆ On)
102		epweon 7793	. . . . . . . . . . . . . . 15 ⊢ E We On
103		wess 5674	. . . . . . . . . . . . . . 15 ⊢ (ran (𝐺‘∪ 𝐶) ⊆ On → ( E We On → E We ran (𝐺‘∪ 𝐶)))
104	101, 102, 103	mpisyl 21	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → E We ran (𝐺‘∪ 𝐶))
105		eqid 2734	. . . . . . . . . . . . . . 15 ⊢ OrdIso( E , ran (𝐺‘∪ 𝐶)) = OrdIso( E , ran (𝐺‘∪ 𝐶))
106	105	oiiso 9574	. . . . . . . . . . . . . 14 ⊢ ((ran (𝐺‘∪ 𝐶) ∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → OrdIso( E , ran (𝐺‘∪ 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)))
107	80, 104, 106	sylancr 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → OrdIso( E , ran (𝐺‘∪ 𝐶)) Isom E , E (dom OrdIso( E , ran (𝐺‘∪ 𝐶)), ran (𝐺‘∪ 𝐶)))
108		isof1o 7342	. . . . . . . . . . . . 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 6860	. . . . . . . . . . . . 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 6847	. . . . . . . . . . . . 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 19	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ◡OrdIso( E , ran (𝐺‘∪ 𝐶)):ran (𝐺‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
112		f1f1orn 6859	. . . . . . . . . . . . 13 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶))
113		f1of1 6847	. . . . . . . . . . . . 13 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶))
114	98, 112, 113	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶))
115		f1co 6815	. . . . . . . . . . . 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 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)):(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
117		dfac12.h	. . . . . . . . . . . 12 ⊢ 𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶))
118		f1eq1 6799	. . . . . . . . . . . 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 234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
121		f1f 6804	. . . . . . . . . 10 ⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → 𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
122		frn 6743	. . . . . . . . . 10 ⊢ (𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
123	120, 121, 122	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
124		harcl 9596	. . . . . . . . . . 11 ⊢ (har‘(𝑅1‘𝐴)) ∈ On
125	124	onordi 6496	. . . . . . . . . 10 ⊢ Ord (har‘(𝑅1‘𝐴))
126	105	oion 9573	. . . . . . . . . . . 12 ⊢ (ran (𝐺‘∪ 𝐶) ∈ V → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
127	80, 126	mp1i 13	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
128	105	oien 9575	. . . . . . . . . . . . 13 ⊢ ((ran (𝐺‘∪ 𝐶) ∈ V ∧ E We ran (𝐺‘∪ 𝐶)) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶))
129	80, 104, 128	sylancr 587	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶))
130		fvex 6919	. . . . . . . . . . . . . . 15 ⊢ (𝑅1‘∪ 𝐶) ∈ V
131	130	f1oen 9011	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶) → (𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶))
132		ensym 9041	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶))
133	98, 112, 131, 132	4syl 19	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶))
134		fvex 6919	. . . . . . . . . . . . . 14 ⊢ (𝑅1‘𝐴) ∈ V
135		dfac12.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ On)
136	135	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐴 ∈ On)
137		dfac12.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
138	137	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ 𝐴)
139	138, 97	sseldd 3995	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐴)
140		r1ord2 9818	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → (∪ 𝐶 ∈ 𝐴 → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴)))
141	136, 139, 140	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴))
142		ssdomg 9038	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘𝐴) ∈ V → ((𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)))
143	134, 141, 142	mpsyl 68	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴))
144		endomtr 9050	. . . . . . . . . . . . 13 ⊢ ((ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶) ∧ (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
145	133, 143, 144	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
146		endomtr 9050	. . . . . . . . . . . 12 ⊢ ((dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≈ ran (𝐺‘∪ 𝐶) ∧ ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼ (𝑅1‘𝐴))
147	129, 145, 146	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼ (𝑅1‘𝐴))
148		elharval 9598	. . . . . . . . . . 11 ⊢ (dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ (har‘(𝑅1‘𝐴)) ↔ (dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ≼ (𝑅1‘𝐴)))
149	127, 147, 148	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ (har‘(𝑅1‘𝐴)))
150		ordelss 6401	. . . . . . . . . 10 ⊢ ((Ord (har‘(𝑅1‘𝐴)) ∧ dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ (har‘(𝑅1‘𝐴))) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ⊆ (har‘(𝑅1‘𝐴)))
151	125, 149, 150	sylancr 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ⊆ (har‘(𝑅1‘𝐴)))
152	123, 151	sstrd 4005	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ (har‘(𝑅1‘𝐴)))
153	78, 152	sstrid 4006	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
154		fvex 6919	. . . . . . . 8 ⊢ (har‘(𝑅1‘𝐴)) ∈ V
155	154	elpw2 5339	. . . . . . 7 ⊢ ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
156	153, 155	sylibr 234	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
157	77, 156	ffvelcdmd 7104	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐹‘(𝐻 “ 𝑦)) ∈ On)
158	73, 157	ifclda 4565	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On)
159	158	ex 412	. . 3 ⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On))
160		iftrue 4536	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)))
161		iftrue 4536	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)))
162	160, 161	eqeq12d 2750	. . . . . . 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 481	. . . . . 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 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
165		nsuceq0 6468	. . . . . . . 8 ⊢ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅
166	165	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅)
167	43	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ On)
168		onsucuni 7847	. . . . . . . . . . 11 ⊢ (ran ∪ (𝐺 “ 𝐶) ⊆ On → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
169	37, 168	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
170	169	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
171	26	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ On)
172		fnfvima 7252	. . . . . . . . . . . 12 ⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
173	2, 171, 63, 172	mp3an2i 1465	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
174		elssuni 4941	. . . . . . . . . . 11 ⊢ ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺 “ 𝐶))
175		rnss 5952	. . . . . . . . . . 11 ⊢ ((𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺 “ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪ (𝐺 “ 𝐶))
176	173, 174, 175	3syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪ (𝐺 “ 𝐶))
177		f1fn 6805	. . . . . . . . . . . 12 ⊢ ((𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
178	64, 177	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)))
179		fnfvelrn 7099	. . . . . . . . . . 11 ⊢ (((𝐺‘suc (rank‘𝑦)) Fn (𝑅1‘suc (rank‘𝑦)) ∧ 𝑦 ∈ (𝑅1‘suc (rank‘𝑦))) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
180	178, 70, 179	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran (𝐺‘suc (rank‘𝑦)))
181	176, 180	sseldd 3995	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran ∪ (𝐺 “ 𝐶))
182	170, 181	sseldd 3995	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
183	182	adantlrr 721	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
184		rankon 9832	. . . . . . . 8 ⊢ (rank‘𝑧) ∈ On
185	184	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑧) ∈ On)
186		eleq1w 2821	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1‘𝐶) ↔ 𝑧 ∈ (𝑅1‘𝐶)))
187	186	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ↔ (𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶))))
188	187	anbi1d 631	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶)))
189		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧))
190		suceq 6451	. . . . . . . . . . . . . 14 ⊢ ((rank‘𝑦) = (rank‘𝑧) → suc (rank‘𝑦) = suc (rank‘𝑧))
191	189, 190	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧))
192	191	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
193		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
194	192, 193	fveq12d 6913	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
195	194	eleq1d 2823	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶) ↔ ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶)))
196	188, 195	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶)) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))))
197	196, 182	chvarvv 1995	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
198	197	adantlrl 720	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
199		omopth2 8620	. . . . . . 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 1385	. . . . . 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 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧))
202	201	fveq2d 6910	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
203	202	fveq1d 6908	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
204	203	eqeq2d 2745	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
205	64	adantlrr 721	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
206	205	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
207	70	adantlrr 721	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
208	207	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
209		r1elwf 9833	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑅1‘𝐶) → 𝑧 ∈ ∪ (𝑅1 “ On))
210		rankidb 9837	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
211	209, 210	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑅1‘𝐶) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
212	211	ad2antll 729	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
213	212	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
214	201	fveq2d 6910	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝑅1‘suc (rank‘𝑦)) = (𝑅1‘suc (rank‘𝑧)))
215	213, 214	eleqtrrd 2841	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))
216		f1fveq 7281	. . . . . . . . . . 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 837	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
218	204, 217	bitr3d 281	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧))
219	218	biimpd 229	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧))
220	219	expimpd 453	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧))
221	189, 194	jca 511	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
222	220, 221	impbid1 225	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧))
223	163, 200, 222	3bitrd 305	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
224		iffalse 4539	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = (𝐹‘(𝐻 “ 𝑦)))
225		iffalse 4539	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = (𝐹‘(𝐻 “ 𝑧)))
226	224, 225	eqeq12d 2750	. . . . . . 7 ⊢ (¬ 𝐶 = ∪ 𝐶 → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧))))
227	226	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧))))
228	74	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On)
229	156	adantlrr 721	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
230	187	anbi1d 631	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶)))
231		imaeq2 6075	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝐻 “ 𝑦) = (𝐻 “ 𝑧))
232	231	eleq1d 2823	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴))))
233	230, 232	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴))) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))))
234	233, 156	chvarvv 1995	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
235	234	adantlrl 720	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
236		f1fveq 7281	. . . . . . 7 ⊢ ((𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On ∧ ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ∧ (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧)))
237	228, 229, 235, 236	syl12anc 837	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧)))
238	120	adantlrr 721	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
239		simplrl 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘𝐶))
240	96	fveq2d 6910	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = (𝑅1‘suc ∪ 𝐶))
241		r1suc 9807	. . . . . . . . . . . 12 ⊢ (∪ 𝐶 ∈ On → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
242	89, 90, 241	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
243	240, 242	eqtrd 2774	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
244	243	adantlrr 721	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
245	239, 244	eleqtrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ∈ 𝒫 (𝑅1‘∪ 𝐶))
246	245	elpwid 4613	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ⊆ (𝑅1‘∪ 𝐶))
247		simplrr 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ (𝑅1‘𝐶))
248	247, 244	eleqtrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ 𝒫 (𝑅1‘∪ 𝐶))
249	248	elpwid 4613	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ⊆ (𝑅1‘∪ 𝐶))
250		f1imaeq 7284	. . . . . . 7 ⊢ ((𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∧ (𝑦 ⊆ (𝑅1‘∪ 𝐶) ∧ 𝑧 ⊆ (𝑅1‘∪ 𝐶))) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧))
251	238, 246, 249, 250	syl12anc 837	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧))
252	227, 237, 251	3bitrd 305	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
253	223, 252	pm2.61dan 813	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
254	253	ex 412	. . 3 ⊢ (𝜑 → ((𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶)) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)))
255	159, 254	dom2lem 9030	. 2 ⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On)
256	135, 74, 1, 5, 117	dfac12lem1 10181	. . 3 ⊢ (𝜑 → (𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))))
257		f1eq1 6799	. . 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 17	. 2 ⊢ (𝜑 → ((𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On ↔ (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On))
259	255, 258	mpbird 257	1 ⊢ (𝜑 → (𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1536   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  Vcvv 3477   ⊆ wss 3962  ∅c0 4338  ifcif 4530  𝒫 cpw 4604  ∪ cuni 4911   class class class wbr 5147   ↦ cmpt 5230   E cep 5587   We wwe 5639   × cxp 5686  ^◡ccnv 5687  dom cdm 5688  ran crn 5689   “ cima 5691   ∘ ccom 5692  Ord word 6384  Oncon0 6385  suc csuc 6387  Fun wfun 6556   Fn wfn 6557  ⟶wf 6558  –1-1→wf1 6559  –1-1-onto→wf1o 6561  ‘cfv 6562   Isom wiso 6563  (class class class)co 7430  recscrecs 8408   +_o coa 8501   ·_o comu 8502   ≈ cen 8980   ≼ cdom 8981  OrdIsocoi 9546  harchar 9593  𝑅₁cr1 9799  rankcrnk 9800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-oadd 8508  df-omul 8509  df-er 8743  df-en 8984  df-dom 8985  df-oi 9547  df-har 9594  df-r1 9801  df-rank 9802

This theorem is referenced by:  dfac12lem3  10183