Theorem dfac12lem2 10080

Description: Lemma for dfac12 10085. (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 8343	. . . . . . . . . . . . 13 ⊢ 𝐺 Fn On
3		fnfun 6602	. . . . . . . . . . . . 13 ⊢ (𝐺 Fn On → Fun 𝐺)
4	2, 3	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun 𝐺
5		dfac12.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ On)
6		funimaexg 6587	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V)
7	4, 5, 6	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ 𝐶) ∈ V)
8		uniexg 7677	. . . . . . . . . . 11 ⊢ ((𝐺 “ 𝐶) ∈ V → ∪ (𝐺 “ 𝐶) ∈ V)
9		rnexg 7841	. . . . . . . . . . 11 ⊢ (∪ (𝐺 “ 𝐶) ∈ V → ran ∪ (𝐺 “ 𝐶) ∈ V)
10	7, 8, 9	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ∈ V)
11		dfac12.8	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
12		f1f 6738	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧):(𝑅1‘𝑧)⟶On)
13		fssxp 6696	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)⟶On → (𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On))
14		ssv 3968	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅1‘𝑧) ⊆ V
15		xpss1 5652	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅1‘𝑧) ⊆ V → ((𝑅1‘𝑧) × On) ⊆ (V × On))
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅1‘𝑧) × On) ⊆ (V × On)
17		sstr 3952	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) ∧ ((𝑅1‘𝑧) × On) ⊆ (V × On)) → (𝐺‘𝑧) ⊆ (V × On))
18	16, 17	mpan2 689	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ⊆ (V × On))
19		fvex 6855	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺‘𝑧) ∈ V
20	19	elpw 4564	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑧) ∈ 𝒫 (V × On) ↔ (𝐺‘𝑧) ⊆ (V × On))
21	18, 20	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧) ⊆ ((𝑅1‘𝑧) × On) → (𝐺‘𝑧) ∈ 𝒫 (V × On))
22	12, 13, 21	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → (𝐺‘𝑧) ∈ 𝒫 (V × On))
23	22	ralimi 3086	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
24	11, 23	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On))
25		onss 7719	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ On → 𝐶 ⊆ On)
26	5, 25	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ⊆ On)
27	2	fndmi 6606	. . . . . . . . . . . . . . . 16 ⊢ dom 𝐺 = On
28	26, 27	sseqtrrdi 3995	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ⊆ dom 𝐺)
29		funimass4 6907	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐺 ∧ 𝐶 ⊆ dom 𝐺) → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On)))
30	4, 28, 29	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∀𝑧 ∈ 𝐶 (𝐺‘𝑧) ∈ 𝒫 (V × On)))
31	24, 30	mpbird 256	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺 “ 𝐶) ⊆ 𝒫 (V × On))
32		sspwuni 5060	. . . . . . . . . . . . 13 ⊢ ((𝐺 “ 𝐶) ⊆ 𝒫 (V × On) ↔ ∪ (𝐺 “ 𝐶) ⊆ (V × On))
33	31, 32	sylib 217	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (𝐺 “ 𝐶) ⊆ (V × On))
34		rnss 5894	. . . . . . . . . . . 12 ⊢ (∪ (𝐺 “ 𝐶) ⊆ (V × On) → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
35	33, 34	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ ran (V × On))
36		rnxpss 6124	. . . . . . . . . . 11 ⊢ ran (V × On) ⊆ On
37	35, 36	sstrdi 3956	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ On)
38		ssonuni 7714	. . . . . . . . . 10 ⊢ (ran ∪ (𝐺 “ 𝐶) ∈ V → (ran ∪ (𝐺 “ 𝐶) ⊆ On → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On))
39	10, 37, 38	sylc 65	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
40		onsuc 7746	. . . . . . . . 9 ⊢ (∪ ran ∪ (𝐺 “ 𝐶) ∈ On → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
41	39, 40	syl 17	. . . . . . . 8 ⊢ (𝜑 → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
42	41	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
43		rankon 9731	. . . . . . 7 ⊢ (rank‘𝑦) ∈ On
44		omcl 8482	. . . . . . 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 6842	. . . . . . . . . . 11 ⊢ (𝑧 = suc (rank‘𝑦) → (𝐺‘𝑧) = (𝐺‘suc (rank‘𝑦)))
47		f1eq1 6733	. . . . . . . . . . 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 6842	. . . . . . . . . . 11 ⊢ (𝑧 = suc (rank‘𝑦) → (𝑅1‘𝑧) = (𝑅1‘suc (rank‘𝑦)))
50		f1eq2 6734	. . . . . . . . . . 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 278	. . . . . . . . 9 ⊢ (𝑧 = suc (rank‘𝑦) → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On))
53	11	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
54		rankr1ai 9734	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → (rank‘𝑦) ∈ 𝐶)
55	54	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ 𝐶)
56		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 = ∪ 𝐶)
57	55, 56	eleqtrd 2840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ ∪ 𝐶)
58		eloni 6327	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → Ord 𝐶)
59	5, 58	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord 𝐶)
60	59	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → Ord 𝐶)
61		ordsucuniel 7759	. . . . . . . . . . 11 ⊢ (Ord 𝐶 → ((rank‘𝑦) ∈ ∪ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
62	60, 61	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((rank‘𝑦) ∈ ∪ 𝐶 ↔ suc (rank‘𝑦) ∈ 𝐶))
63	57, 62	mpbid 231	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → suc (rank‘𝑦) ∈ 𝐶)
64	52, 53, 63	rspcdva 3582	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
65		f1f 6738	. . . . . . . 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 9732	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑅1‘𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
68	67	ad2antlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ ∪ (𝑅1 “ On))
69		rankidb 9736	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ (𝑅1 “ On) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
70	68, 69	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
71	66, 70	ffvelcdmd 7036	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ On)
72		oacl 8481	. . . . . 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 6738	. . . . . . . 8 ⊢ (𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
76	74, 75	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
77	76	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫 (har‘(𝑅1‘𝐴))⟶On)
78		imassrn 6024	. . . . . . . 8 ⊢ (𝐻 “ 𝑦) ⊆ ran 𝐻
79		fvex 6855	. . . . . . . . . . . . . . 15 ⊢ (𝐺‘∪ 𝐶) ∈ V
80	79	rnex 7849	. . . . . . . . . . . . . 14 ⊢ ran (𝐺‘∪ 𝐶) ∈ V
81		fveq2 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∪ 𝐶 → (𝐺‘𝑧) = (𝐺‘∪ 𝐶))
82		f1eq1 6733	. . . . . . . . . . . . . . . . . . 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 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∪ 𝐶 → (𝑅1‘𝑧) = (𝑅1‘∪ 𝐶))
85		f1eq2 6734	. . . . . . . . . . . . . . . . . . 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 278	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∪ 𝐶 → ((𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On ↔ (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On))
88	11	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On)
89	5	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ∈ On)
90		onuni 7723	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ On → ∪ 𝐶 ∈ On)
91		sucidg 6398	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝐶 ∈ On → ∪ 𝐶 ∈ suc ∪ 𝐶)
92	89, 90, 91	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ suc ∪ 𝐶)
93	59	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → Ord 𝐶)
94		orduniorsuc 7765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord 𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
95	93, 94	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶))
96	95	orcanai 1001	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶)
97	92, 96	eleqtrrd 2841	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐶)
98	87, 88, 97	rspcdva 3582	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On)
99		f1f 6738	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On)
100		frn 6675	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)⟶On → ran (𝐺‘∪ 𝐶) ⊆ On)
101	98, 99, 100	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ⊆ On)
102		epweon 7709	. . . . . . . . . . . . . . 15 ⊢ E We On
103		wess 5620	. . . . . . . . . . . . . . 15 ⊢ (ran (𝐺‘∪ 𝐶) ⊆ On → ( E We On → E We ran (𝐺‘∪ 𝐶)))
104	101, 102, 103	mpisyl 21	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → E We ran (𝐺‘∪ 𝐶))
105		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ OrdIso( E , ran (𝐺‘∪ 𝐶)) = OrdIso( E , ran (𝐺‘∪ 𝐶))
106	105	oiiso 9473	. . . . . . . . . . . . . 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 7268	. . . . . . . . . . . . 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 6796	. . . . . . . . . . . . 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 6783	. . . . . . . . . . . . 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 6795	. . . . . . . . . . . . 13 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→On → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶))
113		f1of1 6783	. . . . . . . . . . . . 13 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶))
114	98, 112, 113	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1→ran (𝐺‘∪ 𝐶))
115		f1co 6750	. . . . . . . . . . . 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 6733	. . . . . . . . . . . 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 233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
121		f1f 6738	. . . . . . . . . 10 ⊢ (𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) → 𝐻:(𝑅1‘∪ 𝐶)⟶dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
122		frn 6675	. . . . . . . . . 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 9495	. . . . . . . . . . 11 ⊢ (har‘(𝑅1‘𝐴)) ∈ On
125	124	onordi 6428	. . . . . . . . . 10 ⊢ Ord (har‘(𝑅1‘𝐴))
126	105	oion 9472	. . . . . . . . . . . 12 ⊢ (ran (𝐺‘∪ 𝐶) ∈ V → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
127	80, 126	mp1i 13	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∈ On)
128	105	oien 9474	. . . . . . . . . . . . 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 6855	. . . . . . . . . . . . . . 15 ⊢ (𝑅1‘∪ 𝐶) ∈ V
131	130	f1oen 8913	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘∪ 𝐶):(𝑅1‘∪ 𝐶)–1-1-onto→ran (𝐺‘∪ 𝐶) → (𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶))
132		ensym 8943	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘∪ 𝐶) ≈ ran (𝐺‘∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶))
133	98, 112, 131, 132	4syl 19	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶))
134		fvex 6855	. . . . . . . . . . . . . 14 ⊢ (𝑅1‘𝐴) ∈ V
135		dfac12.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ On)
136	135	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐴 ∈ On)
137		dfac12.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
138	137	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ 𝐴)
139	138, 97	sseldd 3945	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶 ∈ 𝐴)
140		r1ord2 9717	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ On → (∪ 𝐶 ∈ 𝐴 → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴)))
141	136, 139, 140	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴))
142		ssdomg 8940	. . . . . . . . . . . . . 14 ⊢ ((𝑅1‘𝐴) ∈ V → ((𝑅1‘∪ 𝐶) ⊆ (𝑅1‘𝐴) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)))
143	134, 141, 142	mpsyl 68	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴))
144		endomtr 8952	. . . . . . . . . . . . 13 ⊢ ((ran (𝐺‘∪ 𝐶) ≈ (𝑅1‘∪ 𝐶) ∧ (𝑅1‘∪ 𝐶) ≼ (𝑅1‘𝐴)) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
145	133, 143, 144	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran (𝐺‘∪ 𝐶) ≼ (𝑅1‘𝐴))
146		endomtr 8952	. . . . . . . . . . . 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 9497	. . . . . . . . . . 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 6333	. . . . . . . . . 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 3954	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ran 𝐻 ⊆ (har‘(𝑅1‘𝐴)))
153	78, 152	sstrid 3955	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
154		fvex 6855	. . . . . . . 8 ⊢ (har‘(𝑅1‘𝐴)) ∈ V
155	154	elpw2 5302	. . . . . . 7 ⊢ ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑦) ⊆ (har‘(𝑅1‘𝐴)))
156	153, 155	sylibr 233	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
157	77, 156	ffvelcdmd 7036	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐹‘(𝐻 “ 𝑦)) ∈ On)
158	73, 157	ifclda 4521	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On)
159	158	ex 413	. . 3 ⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) ∈ On))
160		iftrue 4492	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)))
161		iftrue 4492	. . . . . . . 8 ⊢ (𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)))
162	160, 161	eqeq12d 2752	. . . . . . 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 482	. . . . . 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 724	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ∈ On)
165		nsuceq0 6400	. . . . . . . 8 ⊢ suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅
166	165	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → suc ∪ ran ∪ (𝐺 “ 𝐶) ≠ ∅)
167	43	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑦) ∈ On)
168		onsucuni 7763	. . . . . . . . . . 11 ⊢ (ran ∪ (𝐺 “ 𝐶) ⊆ On → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
169	37, 168	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
170	169	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran ∪ (𝐺 “ 𝐶) ⊆ suc ∪ ran ∪ (𝐺 “ 𝐶))
171	26	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → 𝐶 ⊆ On)
172		fnfvima 7183	. . . . . . . . . . . 12 ⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On ∧ suc (rank‘𝑦) ∈ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
173	2, 171, 63, 172	mp3an2i 1466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶))
174		elssuni 4898	. . . . . . . . . . 11 ⊢ ((𝐺‘suc (rank‘𝑦)) ∈ (𝐺 “ 𝐶) → (𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺 “ 𝐶))
175		rnss 5894	. . . . . . . . . . 11 ⊢ ((𝐺‘suc (rank‘𝑦)) ⊆ ∪ (𝐺 “ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪ (𝐺 “ 𝐶))
176	173, 174, 175	3syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ran (𝐺‘suc (rank‘𝑦)) ⊆ ran ∪ (𝐺 “ 𝐶))
177		f1fn 6739	. . . . . . . . . . . 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 7031	. . . . . . . . . . 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 3945	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ ran ∪ (𝐺 “ 𝐶))
182	170, 181	sseldd 3945	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
183	182	adantlrr 719	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑦))‘𝑦) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
184		rankon 9731	. . . . . . . 8 ⊢ (rank‘𝑧) ∈ On
185	184	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (rank‘𝑧) ∈ On)
186		eleq1w 2820	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝑅1‘𝐶) ↔ 𝑧 ∈ (𝑅1‘𝐶)))
187	186	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ↔ (𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶))))
188	187	anbi1d 630	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶)))
189		fveq2 6842	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (rank‘𝑦) = (rank‘𝑧))
190		suceq 6383	. . . . . . . . . . . . . 14 ⊢ ((rank‘𝑦) = (rank‘𝑧) → suc (rank‘𝑦) = suc (rank‘𝑧))
191	189, 190	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → suc (rank‘𝑦) = suc (rank‘𝑧))
192	191	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
193		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
194	192, 193	fveq12d 6849	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
195	194	eleq1d 2822	. . . . . . . . . 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 2002	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
198	197	adantlrl 718	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → ((𝐺‘suc (rank‘𝑧))‘𝑧) ∈ suc ∪ ran ∪ (𝐺 “ 𝐶))
199		omopth2 8531	. . . . . . 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 1386	. . . . . 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 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → suc (rank‘𝑦) = suc (rank‘𝑧))
202	201	fveq2d 6846	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)) = (𝐺‘suc (rank‘𝑧)))
203	202	fveq1d 6844	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → ((𝐺‘suc (rank‘𝑦))‘𝑧) = ((𝐺‘suc (rank‘𝑧))‘𝑧))
204	203	eqeq2d 2747	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
205	64	adantlrr 719	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
206	205	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (𝐺‘suc (rank‘𝑦)):(𝑅1‘suc (rank‘𝑦))–1-1→On)
207	70	adantlrr 719	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
208	207	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑦 ∈ (𝑅1‘suc (rank‘𝑦)))
209		r1elwf 9732	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑅1‘𝐶) → 𝑧 ∈ ∪ (𝑅1 “ On))
210		rankidb 9736	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ∪ (𝑅1 “ On) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
211	209, 210	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑅1‘𝐶) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
212	211	ad2antll 727	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
213	212	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → 𝑧 ∈ (𝑅1‘suc (rank‘𝑧)))
214	201	fveq2d 6846	. . . . . . . . . . . 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 7209	. . . . . . . . . . 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 835	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑦))‘𝑧) ↔ 𝑦 = 𝑧))
218	204, 217	bitr3d 280	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) ↔ 𝑦 = 𝑧))
219	218	biimpd 228	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) ∧ (rank‘𝑦) = (rank‘𝑧)) → (((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧) → 𝑦 = 𝑧))
220	219	expimpd 454	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) → 𝑦 = 𝑧))
221	189, 194	jca 512	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)))
222	220, 221	impbid1 224	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (((rank‘𝑦) = (rank‘𝑧) ∧ ((𝐺‘suc (rank‘𝑦))‘𝑦) = ((𝐺‘suc (rank‘𝑧))‘𝑧)) ↔ 𝑦 = 𝑧))
223	163, 200, 222	3bitrd 304	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
224		iffalse 4495	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = (𝐹‘(𝐻 “ 𝑦)))
225		iffalse 4495	. . . . . . . 8 ⊢ (¬ 𝐶 = ∪ 𝐶 → if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) = (𝐹‘(𝐻 “ 𝑧)))
226	224, 225	eqeq12d 2752	. . . . . . 7 ⊢ (¬ 𝐶 = ∪ 𝐶 → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧))))
227	226	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ (𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧))))
228	74	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On)
229	156	adantlrr 719	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
230	187	anbi1d 630	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) ↔ ((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶)))
231		imaeq2 6009	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝐻 “ 𝑦) = (𝐻 “ 𝑧))
232	231	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ↔ (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴))))
233	230, 232	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴))) ↔ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))))
234	233, 156	chvarvv 2002	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
235	234	adantlrl 718	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))
236		f1fveq 7209	. . . . . . 7 ⊢ ((𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On ∧ ((𝐻 “ 𝑦) ∈ 𝒫 (har‘(𝑅1‘𝐴)) ∧ (𝐻 “ 𝑧) ∈ 𝒫 (har‘(𝑅1‘𝐴)))) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧)))
237	228, 229, 235, 236	syl12anc 835	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐹‘(𝐻 “ 𝑦)) = (𝐹‘(𝐻 “ 𝑧)) ↔ (𝐻 “ 𝑦) = (𝐻 “ 𝑧)))
238	120	adantlrr 719	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)))
239		simplrl 775	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ∈ (𝑅1‘𝐶))
240	96	fveq2d 6846	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = (𝑅1‘suc ∪ 𝐶))
241		r1suc 9706	. . . . . . . . . . . 12 ⊢ (∪ 𝐶 ∈ On → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
242	89, 90, 241	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘suc ∪ 𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
243	240, 242	eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑅1‘𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
244	243	adantlrr 719	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (𝑅1‘𝐶) = 𝒫 (𝑅1‘∪ 𝐶))
245	239, 244	eleqtrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ∈ 𝒫 (𝑅1‘∪ 𝐶))
246	245	elpwid 4569	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑦 ⊆ (𝑅1‘∪ 𝐶))
247		simplrr 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ (𝑅1‘𝐶))
248	247, 244	eleqtrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ∈ 𝒫 (𝑅1‘∪ 𝐶))
249	248	elpwid 4569	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝑧 ⊆ (𝑅1‘∪ 𝐶))
250		f1imaeq 7212	. . . . . . 7 ⊢ ((𝐻:(𝑅1‘∪ 𝐶)–1-1→dom OrdIso( E , ran (𝐺‘∪ 𝐶)) ∧ (𝑦 ⊆ (𝑅1‘∪ 𝐶) ∧ 𝑧 ⊆ (𝑅1‘∪ 𝐶))) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧))
251	238, 246, 249, 250	syl12anc 835	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐻 “ 𝑦) = (𝐻 “ 𝑧) ↔ 𝑦 = 𝑧))
252	227, 237, 251	3bitrd 304	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) ∧ ¬ 𝐶 = ∪ 𝐶) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
253	223, 252	pm2.61dan 811	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶))) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧))
254	253	ex 413	. . 3 ⊢ (𝜑 → ((𝑦 ∈ (𝑅1‘𝐶) ∧ 𝑧 ∈ (𝑅1‘𝐶)) → (if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))) = if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑧)) +o ((𝐺‘suc (rank‘𝑧))‘𝑧)), (𝐹‘(𝐻 “ 𝑧))) ↔ 𝑦 = 𝑧)))
255	159, 254	dom2lem 8932	. 2 ⊢ (𝜑 → (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))):(𝑅1‘𝐶)–1-1→On)
256	135, 74, 1, 5, 117	dfac12lem1 10079	. . 3 ⊢ (𝜑 → (𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦)))))
257		f1eq1 6733	. . 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 256	1 ⊢ (𝜑 → (𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  Vcvv 3445   ⊆ wss 3910  ∅c0 4282  ifcif 4486  𝒫 cpw 4560  ∪ cuni 4865   class class class wbr 5105   ↦ cmpt 5188   E cep 5536   We wwe 5587   × cxp 5631  ^◡ccnv 5632  dom cdm 5633  ran crn 5634   “ cima 5636   ∘ ccom 5637  Ord word 6316  Oncon0 6317  suc csuc 6319  Fun wfun 6490   Fn wfn 6491  ⟶wf 6492  –1-1→wf1 6493  –1-1-onto→wf1o 6495  ‘cfv 6496   Isom wiso 6497  (class class class)co 7357  recscrecs 8316   +_o coa 8409   ·_o comu 8410   ≈ cen 8880   ≼ cdom 8881  OrdIsocoi 9445  harchar 9492  𝑅₁cr1 9698  rankcrnk 9699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-oadd 8416  df-omul 8417  df-er 8648  df-en 8884  df-dom 8885  df-oi 9446  df-har 9493  df-r1 9700  df-rank 9701

This theorem is referenced by:  dfac12lem3  10081