Theorem dfac12lem2 10185

Description: Lemma for dfac12 10190. (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 8437	. . . . . . . . . . . . 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 7760	. . . . . . . . . . 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 4008	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅1‘𝑧) ⊆ V
15		xpss1 5704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅1‘𝑧) ⊆ V → ((𝑅1‘𝑧) × On) ⊆ (V × On))
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅1‘𝑧) × On) ⊆ (V × On)
17		sstr 3992	. . . . . . . . . . . . . . . . . . 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 4604	. . . . . . . . . . . . . . . . . 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 3083	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
24	11, 23	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
25		onss 7805	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ On → 𝐶 ⊆ On)
26	5, 25	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ⊆ On)
27	2	fndmi 6672	. . . . . . . . . . . . . . . 16 ⊢ dom 𝐺 = On
28	26, 27	sseqtrrdi 4025	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ⊆ dom 𝐺)
29		funimass4 6973	. . . . . . . . . . . . . . 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 5100	. . . . . . . . . . . . 13 ⊢ ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∪ (𝐺 “ 𝐶) ⊆ (V × On))
33	31, 32	sylib 218	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (𝐺 “ 𝐶) ⊆ (V × On))
34		rnss 5950	. . . . . . . . . . . 12 ⊢ (∪ (𝐺 “ 𝐶) ⊆ (V × On) → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
35	33, 34	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
36		rnxpss 6192	. . . . . . . . . . 11 ⊢ ran (V × On) ⊆ On
37	35, 36	sstrdi 3996	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ On)
38		ssonuni 7800	. . . . . . . . . 10 ⊢ (ran ∪ (𝐺 “ 𝐶) ∈ V → (ran ∪ (𝐺 “ 𝐶) ⊆ On → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On))
39	10, 37, 38	sylc 65	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
40		onsuc 7831	. . . . . . . . 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 9835	. . . . . . 7 ⊢ (rank‘𝑦) ∈ On
44		omcl 8574	. . . . . . 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 9838	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → (rank‘𝑦) ∈ 𝐶)
55	54	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ 𝐶)
56		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 = ∪ 𝐶)
57	55, 56	eleqtrd 2843	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ ∪ 𝐶)
58		eloni 6394	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
59	5, 58	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord 𝐶)
60	59	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → Ord 𝐶)
61		ordsucuniel 7844	. . . . . . . . . . 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 3623	. . . . . . . 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 9836	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
68	67	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
69		rankidb 9840	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
70	68, 69	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
71	66, 70	ffvelcdmd 7105	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On)
72		oacl 8573	. . . . . 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 6089	. . . . . . . 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 7808	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ On → ∪ 𝐶 ∈ On)
91		sucidg 6465	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝐶 ∈ On → ∪ 𝐶 ∈ suc ∪ 𝐶)
92	89, 90, 91	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ suc ∪ 𝐶)
93	59	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → Ord 𝐶)
94		orduniorsuc 7850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
95	93, 94	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
96	95	orcanai 1005	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶)
97	92, 96	eleqtrrd 2844	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐶)
98	87, 88, 97	rspcdva 3623	. . . . . . . . . . . . . . . 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 7795	. . . . . . . . . . . . . . 15 ⊢ E We On
103		wess 5671	. . . . . . . . . . . . . . 15 ⊢ (ran (𝐺‘∪ 𝐶) ⊆ On → ( E We On → E We ran (𝐺‘∪ 𝐶)))
104	101, 102, 103	mpisyl 21	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → E We ran (𝐺‘∪ 𝐶))
105		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ OrdIso( E , ran (𝐺‘∪ 𝐶)) = OrdIso( E , ran (𝐺‘∪ 𝐶))
106	105	oiiso 9577	. . . . . . . . . . . . . 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 7343	. . . . . . . . . . . . 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 9599	. . . . . . . . . . 11 ⊢ (har‘(𝑅1‘𝐴)) ∈ On
125	124	onordi 6495	. . . . . . . . . 10 ⊢ Ord (har‘(𝑅1‘𝐴))
126	105	oion 9576	. . . . . . . . . . . 12 ⊢ (ran (𝐺‘∪ 𝐶) ∈ V → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
127	80, 126	mp1i 13	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
128	105	oien 9578	. . . . . . . . . . . . 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 9013	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶) → (𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶))
132		ensym 9043	. . . . . . . . . . . . . 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 3984	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐴)
140		r1ord2 9821	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → (∪ 𝐶 ∈ 𝐴 → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴)))
141	136, 139, 140	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴))
142		ssdomg 9040	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘𝐴) ∈ V → ((𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)))
143	134, 141, 142	mpsyl 68	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴))
144		endomtr 9052	. . . . . . . . . . . . 13 ⊢ ((ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶) ∧ (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
145	133, 143, 144	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
146		endomtr 9052	. . . . . . . . . . . 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 9601	. . . . . . . . . . 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 6400	. . . . . . . . . 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 3994	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ (har‘(𝑅1‘𝐴)))
153	78, 152	sstrid 3995	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
154		fvex 6919	. . . . . . . 8 ⊢ (har‘(𝑅1‘𝐴)) ∈ V
155	154	elpw2 5334	. . . . . . 7 ⊢ ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
156	153, 155	sylibr 234	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
157	77, 156	ffvelcdmd 7105	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐹‘(𝐻 “ 𝑦)) ∈ On)
158	73, 157	ifclda 4561	. . . 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 4531	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)))
161		iftrue 4531	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)))
162	160, 161	eqeq12d 2753	. . . . . . 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 6467	. . . . . . . 8 ⊢ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅
166	165	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅)
167	43	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ On)
168		onsucuni 7848	. . . . . . . . . . 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 7253	. . . . . . . . . . . 12 ⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
173	2, 171, 63, 172	mp3an2i 1468	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
174		elssuni 4937	. . . . . . . . . . 11 ⊢ ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺 “ 𝐶))
175		rnss 5950	. . . . . . . . . . 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 7100	. . . . . . . . . . 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 3984	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran ∪ (𝐺 “ 𝐶))
182	170, 181	sseldd 3984	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
183	182	adantlrr 721	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
184		rankon 9835	. . . . . . . 8 ⊢ (rank‘𝑧) ∈ On
185	184	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑧) ∈ On)
186		eleq1w 2824	. . . . . . . . . . . 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 6450	. . . . . . . . . . . . . 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 2826	. . . . . . . . . 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 1998	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
198	197	adantlrl 720	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
199		omopth2 8622	. . . . . . 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 1388	. . . . . 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 2748	. . . . . . . . . 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 9836	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑅1‘𝐶) → 𝑧 ∈ ∪ (𝑅1 “ On))
210		rankidb 9840	. . . . . . . . . . . . . . 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 2844	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑦)))
216		f1fveq 7282	. . . . . . . . . . 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 4534	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = (𝐹‘(𝐻 “ 𝑦)))
225		iffalse 4534	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = (𝐹‘(𝐻 “ 𝑧)))
226	224, 225	eqeq12d 2753	. . . . . . 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 6074	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝐻 “ 𝑦) = (𝐻 “ 𝑧))
232	231	eleq1d 2826	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴))))
233	230, 232	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴))) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))))
234	233, 156	chvarvv 1998	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
235	234	adantlrl 720	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
236		f1fveq 7282	. . . . . . 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 9810	. . . . . . . . . . . 12 ⊢ (∪ 𝐶 ∈ On → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
242	89, 90, 241	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
243	240, 242	eqtrd 2777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
244	243	adantlrr 721	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
245	239, 244	eleqtrd 2843	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ∈ 𝒫 (𝑅1‘∪ 𝐶))
246	245	elpwid 4609	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ⊆ (𝑅1‘∪ 𝐶))
247		simplrr 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ (𝑅1‘𝐶))
248	247, 244	eleqtrd 2843	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ 𝒫 (𝑅1‘∪ 𝐶))
249	248	elpwid 4609	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ⊆ (𝑅1‘∪ 𝐶))
250		f1imaeq 7285	. . . . . . 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 9032	. 2 ⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On)
256	135, 74, 1, 5, 117	dfac12lem1 10184	. . 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 848   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  Vcvv 3480   ⊆ wss 3951  ∅c0 4333  ifcif 4525  𝒫 cpw 4600  ∪ cuni 4907   class class class wbr 5143   ↦ cmpt 5225   E cep 5583   We wwe 5636   × cxp 5683  ^◡ccnv 5684  dom cdm 5685  ran crn 5686   “ cima 5688   ∘ ccom 5689  Ord word 6383  Oncon0 6384  suc csuc 6386  Fun wfun 6555   Fn wfn 6556  ⟶wf 6557  –1-1→wf1 6558  –1-1-onto→wf1o 6560  ‘cfv 6561   Isom wiso 6562  (class class class)co 7431  recscrecs 8410   +_o coa 8503   ·_o comu 8504   ≈ cen 8982   ≼ cdom 8983  OrdIsocoi 9549  harchar 9596  𝑅₁cr1 9802  rankcrnk 9803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-oadd 8510  df-omul 8511  df-er 8745  df-en 8986  df-dom 8987  df-oi 9550  df-har 9597  df-r1 9804  df-rank 9805

This theorem is referenced by:  dfac12lem3  10186