dfac12lem2

	Ref	Expression
Hypotheses	dfac12.1	$⊢ φ \to A \in On$
	dfac12.3	$⊢ φ \to F : 𝒫 har (R_{1} (A)) \underset{1-1}{⟶} On$
	dfac12.4	$⊢ G = recs ((x \in V ⟼ (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), F (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y])))))$
	dfac12.5	$⊢ φ \to C \in On$
	dfac12.h	$⊢ H = {OrdIso (E, ran G (⋃ C))}^{-1} \circ G (⋃ C)$
	dfac12.6	$⊢ φ \to C \subseteq A$
	dfac12.8	$⊢ φ \to \forall z \in C G (z) : R_{1} (z) \underset{1-1}{⟶} On$
Assertion	dfac12lem2	$⊢ φ \to G (C) : R_{1} (C) \underset{1-1}{⟶} On$

Proof

Step	Hyp	Ref	Expression
1		dfac12.1	$⊢ φ \to A \in On$
2		dfac12.3	$⊢ φ \to F : 𝒫 har (R_{1} (A)) \underset{1-1}{⟶} On$
3		dfac12.4	$⊢ G = recs ((x \in V ⟼ (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), F (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y])))))$
4		dfac12.5	$⊢ φ \to C \in On$
5		dfac12.h	$⊢ H = {OrdIso (E, ran G (⋃ C))}^{-1} \circ G (⋃ C)$
6		dfac12.6	$⊢ φ \to C \subseteq A$
7		dfac12.8	$⊢ φ \to \forall z \in C G (z) : R_{1} (z) \underset{1-1}{⟶} On$
8	3	tfr1	$⊢ G Fn On$
9		fnfun	$⊢ G Fn On \to Fun G$
10	8 9	ax-mp	$⊢ Fun G$
11		funimaexg	$⊢ (Fun G \land C \in On) \to G [C] \in V$
12	10 4 11	sylancr	$⊢ φ \to G [C] \in V$
13		uniexg	$⊢ G [C] \in V \to ⋃ G [C] \in V$
14		rnexg	$⊢ ⋃ G [C] \in V \to ran ⋃ G [C] \in V$
15	12 13 14	3syl	$⊢ φ \to ran ⋃ G [C] \in V$
16		f1f	$⊢ G (z) : R_{1} (z) \underset{1-1}{⟶} On \to G (z) : R_{1} (z) ⟶ On$
17		fssxp	$⊢ G (z) : R_{1} (z) ⟶ On \to G (z) \subseteq R_{1} (z) \times On$
18		ssv	$⊢ R_{1} (z) \subseteq V$
19		xpss1	$⊢ R_{1} (z) \subseteq V \to R_{1} (z) \times On \subseteq V \times On$
20	18 19	ax-mp	$⊢ R_{1} (z) \times On \subseteq V \times On$
21		sstr	$⊢ (G (z) \subseteq R_{1} (z) \times On \land R_{1} (z) \times On \subseteq V \times On) \to G (z) \subseteq V \times On$
22	20 21	mpan2	$⊢ G (z) \subseteq R_{1} (z) \times On \to G (z) \subseteq V \times On$
23		fvex	$⊢ G (z) \in V$
24	23	elpw	$⊢ G (z) \in 𝒫 (V \times On) \leftrightarrow G (z) \subseteq V \times On$
25	22 24	sylibr	$⊢ G (z) \subseteq R_{1} (z) \times On \to G (z) \in 𝒫 (V \times On)$
26	16 17 25	3syl	$⊢ G (z) : R_{1} (z) \underset{1-1}{⟶} On \to G (z) \in 𝒫 (V \times On)$
27	26	ralimi	$⊢ \forall z \in C G (z) : R_{1} (z) \underset{1-1}{⟶} On \to \forall z \in C G (z) \in 𝒫 (V \times On)$
28	7 27	syl	$⊢ φ \to \forall z \in C G (z) \in 𝒫 (V \times On)$
29		onss	$⊢ C \in On \to C \subseteq On$
30	4 29	syl	$⊢ φ \to C \subseteq On$
31		fndm	$⊢ G Fn On \to dom G = On$
32	8 31	ax-mp	$⊢ dom G = On$
33	30 32	sseqtrrdi	$⊢ φ \to C \subseteq dom G$
34		funimass4	$⊢ (Fun G \land C \subseteq dom G) \to (G [C] \subseteq 𝒫 (V \times On) \leftrightarrow \forall z \in C G (z) \in 𝒫 (V \times On))$
35	10 33 34	sylancr	$⊢ φ \to (G [C] \subseteq 𝒫 (V \times On) \leftrightarrow \forall z \in C G (z) \in 𝒫 (V \times On))$
36	28 35	mpbird	$⊢ φ \to G [C] \subseteq 𝒫 (V \times On)$
37		sspwuni	$⊢ G [C] \subseteq 𝒫 (V \times On) \leftrightarrow ⋃ G [C] \subseteq V \times On$
38	36 37	sylib	$⊢ φ \to ⋃ G [C] \subseteq V \times On$
39		rnss	$⊢ ⋃ G [C] \subseteq V \times On \to ran ⋃ G [C] \subseteq ran (V \times On)$
40	38 39	syl	$⊢ φ \to ran ⋃ G [C] \subseteq ran (V \times On)$
41		rnxpss	$⊢ ran (V \times On) \subseteq On$
42	40 41	sstrdi	$⊢ φ \to ran ⋃ G [C] \subseteq On$
43		ssonuni	$⊢ ran ⋃ G [C] \in V \to (ran ⋃ G [C] \subseteq On \to ⋃ ran ⋃ G [C] \in On)$
44	15 42 43	sylc	$⊢ φ \to ⋃ ran ⋃ G [C] \in On$
45		suceloni	$⊢ ⋃ ran ⋃ G [C] \in On \to suc ⋃ ran ⋃ G [C] \in On$
46	44 45	syl	$⊢ φ \to suc ⋃ ran ⋃ G [C] \in On$
47	46	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to suc ⋃ ran ⋃ G [C] \in On$
48		rankon	$⊢ rank (y) \in On$
49		omcl	$⊢ (suc ⋃ ran ⋃ G [C] \in On \land rank (y) \in On) \to suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y) \in On$
50	47 48 49	sylancl	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y) \in On$
51		fveq2	$⊢ z = suc rank (y) \to G (z) = G (suc rank (y))$
52		f1eq1	$⊢ G (z) = G (suc rank (y)) \to (G (z) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (suc rank (y)) : R_{1} (z) \underset{1-1}{⟶} On)$
53	51 52	syl	$⊢ z = suc rank (y) \to (G (z) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (suc rank (y)) : R_{1} (z) \underset{1-1}{⟶} On)$
54		fveq2	$⊢ z = suc rank (y) \to R_{1} (z) = R_{1} (suc rank (y))$
55		f1eq2	$⊢ R_{1} (z) = R_{1} (suc rank (y)) \to (G (suc rank (y)) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (suc rank (y)) : R_{1} (suc rank (y)) \underset{1-1}{⟶} On)$
56	54 55	syl	$⊢ z = suc rank (y) \to (G (suc rank (y)) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (suc rank (y)) : R_{1} (suc rank (y)) \underset{1-1}{⟶} On)$
57	53 56	bitrd	$⊢ z = suc rank (y) \to (G (z) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (suc rank (y)) : R_{1} (suc rank (y)) \underset{1-1}{⟶} On)$
58	7	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to \forall z \in C G (z) : R_{1} (z) \underset{1-1}{⟶} On$
59		rankr1ai	$⊢ y \in R_{1} (C) \to rank (y) \in C$
60	59	ad2antlr	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to rank (y) \in C$
61		simpr	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to C = ⋃ C$
62	60 61	eleqtrd	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to rank (y) \in ⋃ C$
63		eloni	$⊢ C \in On \to Ord C$
64	4 63	syl	$⊢ φ \to Ord C$
65	64	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to Ord C$
66		ordsucuniel	$⊢ Ord C \to (rank (y) \in ⋃ C \leftrightarrow suc rank (y) \in C)$
67	65 66	syl	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to (rank (y) \in ⋃ C \leftrightarrow suc rank (y) \in C)$
68	62 67	mpbid	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to suc rank (y) \in C$
69	57 58 68	rspcdva	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (y)) : R_{1} (suc rank (y)) \underset{1-1}{⟶} On$
70		f1f	$⊢ G (suc rank (y)) : R_{1} (suc rank (y)) \underset{1-1}{⟶} On \to G (suc rank (y)) : R_{1} (suc rank (y)) ⟶ On$
71	69 70	syl	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (y)) : R_{1} (suc rank (y)) ⟶ On$
72		r1elwf	$⊢ y \in R_{1} (C) \to y \in ⋃ R_{1} [On]$
73	72	ad2antlr	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to y \in ⋃ R_{1} [On]$
74		rankidb	$⊢ y \in ⋃ R_{1} [On] \to y \in R_{1} (suc rank (y))$
75	73 74	syl	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to y \in R_{1} (suc rank (y))$
76	71 75	ffvelrnd	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (y)) (y) \in On$
77		oacl	$⊢ (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y) \in On \land G (suc rank (y)) (y) \in On) \to (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y) \in On$
78	50 76 77	syl2anc	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y) \in On$
79		f1f	$⊢ F : 𝒫 har (R_{1} (A)) \underset{1-1}{⟶} On \to F : 𝒫 har (R_{1} (A)) ⟶ On$
80	2 79	syl	$⊢ φ \to F : 𝒫 har (R_{1} (A)) ⟶ On$
81	80	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to F : 𝒫 har (R_{1} (A)) ⟶ On$
82		imassrn	$⊢ H [y] \subseteq ran H$
83		fvex	$⊢ G (⋃ C) \in V$
84	83	rnex	$⊢ ran G (⋃ C) \in V$
85		fveq2	$⊢ z = ⋃ C \to G (z) = G (⋃ C)$
86		f1eq1	$⊢ G (z) = G (⋃ C) \to (G (z) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (⋃ C) : R_{1} (z) \underset{1-1}{⟶} On)$
87	85 86	syl	$⊢ z = ⋃ C \to (G (z) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (⋃ C) : R_{1} (z) \underset{1-1}{⟶} On)$
88		fveq2	$⊢ z = ⋃ C \to R_{1} (z) = R_{1} (⋃ C)$
89		f1eq2	$⊢ R_{1} (z) = R_{1} (⋃ C) \to (G (⋃ C) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (⋃ C) : R_{1} (⋃ C) \underset{1-1}{⟶} On)$
90	88 89	syl	$⊢ z = ⋃ C \to (G (⋃ C) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (⋃ C) : R_{1} (⋃ C) \underset{1-1}{⟶} On)$
91	87 90	bitrd	$⊢ z = ⋃ C \to (G (z) : R_{1} (z) \underset{1-1}{⟶} On \leftrightarrow G (⋃ C) : R_{1} (⋃ C) \underset{1-1}{⟶} On)$
92	7	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to \forall z \in C G (z) : R_{1} (z) \underset{1-1}{⟶} On$
93	4	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to C \in On$
94		onuni	$⊢ C \in On \to ⋃ C \in On$
95		sucidg	$⊢ ⋃ C \in On \to ⋃ C \in suc ⋃ C$
96	93 94 95	3syl	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to ⋃ C \in suc ⋃ C$
97	64	adantr	$⊢ (φ \land y \in R_{1} (C)) \to Ord C$
98		orduniorsuc	$⊢ Ord C \to (C = ⋃ C \lor C = suc ⋃ C)$
99	97 98	syl	$⊢ (φ \land y \in R_{1} (C)) \to (C = ⋃ C \lor C = suc ⋃ C)$
100	99	orcanai	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to C = suc ⋃ C$
101	96 100	eleqtrrd	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to ⋃ C \in C$
102	91 92 101	rspcdva	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to G (⋃ C) : R_{1} (⋃ C) \underset{1-1}{⟶} On$
103		f1f	$⊢ G (⋃ C) : R_{1} (⋃ C) \underset{1-1}{⟶} On \to G (⋃ C) : R_{1} (⋃ C) ⟶ On$
104		frn	$⊢ G (⋃ C) : R_{1} (⋃ C) ⟶ On \to ran G (⋃ C) \subseteq On$
105	102 103 104	3syl	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to ran G (⋃ C) \subseteq On$
106		epweon	$⊢ E We On$
107		wess	$⊢ ran G (⋃ C) \subseteq On \to (E We On \to E We ran G (⋃ C))$
108	105 106 107	mpisyl	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to E We ran G (⋃ C)$
109		eqid	$⊢ OrdIso (E, ran G (⋃ C)) = OrdIso (E, ran G (⋃ C))$
110	109	oiiso	$⊢ (ran G (⋃ C) \in V \land E We ran G (⋃ C)) \to OrdIso (E, ran G (⋃ C)) {Isom}_{E, E} (dom OrdIso (E, ran G (⋃ C)), ran G (⋃ C))$
111	84 108 110	sylancr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to OrdIso (E, ran G (⋃ C)) {Isom}_{E, E} (dom OrdIso (E, ran G (⋃ C)), ran G (⋃ C))$
112		isof1o	$⊢ OrdIso (E, ran G (⋃ C)) {Isom}_{E, E} (dom OrdIso (E, ran G (⋃ C)), ran G (⋃ C)) \to OrdIso (E, ran G (⋃ C)) : dom OrdIso (E, ran G (⋃ C)) \underset{1-1 onto}{⟶} ran G (⋃ C)$
113		f1ocnv	$⊢ OrdIso (E, ran G (⋃ C)) : dom OrdIso (E, ran G (⋃ C)) \underset{1-1 onto}{⟶} ran G (⋃ C) \to {OrdIso (E, ran G (⋃ C))}^{-1} : ran G (⋃ C) \underset{1-1 onto}{⟶} dom OrdIso (E, ran G (⋃ C))$
114		f1of1	$⊢ {OrdIso (E, ran G (⋃ C))}^{-1} : ran G (⋃ C) \underset{1-1 onto}{⟶} dom OrdIso (E, ran G (⋃ C)) \to {OrdIso (E, ran G (⋃ C))}^{-1} : ran G (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C))$
115	111 112 113 114	4syl	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to {OrdIso (E, ran G (⋃ C))}^{-1} : ran G (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C))$
116		f1f1orn	$⊢ G (⋃ C) : R_{1} (⋃ C) \underset{1-1}{⟶} On \to G (⋃ C) : R_{1} (⋃ C) \underset{1-1 onto}{⟶} ran G (⋃ C)$
117		f1of1	$⊢ G (⋃ C) : R_{1} (⋃ C) \underset{1-1 onto}{⟶} ran G (⋃ C) \to G (⋃ C) : R_{1} (⋃ C) \underset{1-1}{⟶} ran G (⋃ C)$
118	102 116 117	3syl	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to G (⋃ C) : R_{1} (⋃ C) \underset{1-1}{⟶} ran G (⋃ C)$
119		f1co	$⊢ ({OrdIso (E, ran G (⋃ C))}^{-1} : ran G (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C)) \land G (⋃ C) : R_{1} (⋃ C) \underset{1-1}{⟶} ran G (⋃ C)) \to ({OrdIso (E, ran G (⋃ C))}^{-1} \circ G (⋃ C)) : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C))$
120	115 118 119	syl2anc	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to ({OrdIso (E, ran G (⋃ C))}^{-1} \circ G (⋃ C)) : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C))$
121		f1eq1	$⊢ H = {OrdIso (E, ran G (⋃ C))}^{-1} \circ G (⋃ C) \to (H : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C)) \leftrightarrow ({OrdIso (E, ran G (⋃ C))}^{-1} \circ G (⋃ C)) : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C)))$
122	5 121	ax-mp	$⊢ H : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C)) \leftrightarrow ({OrdIso (E, ran G (⋃ C))}^{-1} \circ G (⋃ C)) : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C))$
123	120 122	sylibr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to H : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C))$
124		f1f	$⊢ H : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C)) \to H : R_{1} (⋃ C) ⟶ dom OrdIso (E, ran G (⋃ C))$
125		frn	$⊢ H : R_{1} (⋃ C) ⟶ dom OrdIso (E, ran G (⋃ C)) \to ran H \subseteq dom OrdIso (E, ran G (⋃ C))$
126	123 124 125	3syl	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to ran H \subseteq dom OrdIso (E, ran G (⋃ C))$
127		harcl	$⊢ har (R_{1} (A)) \in On$
128	127	onordi	$⊢ Ord har (R_{1} (A))$
129	109	oion	$⊢ ran G (⋃ C) \in V \to dom OrdIso (E, ran G (⋃ C)) \in On$
130	84 129	mp1i	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to dom OrdIso (E, ran G (⋃ C)) \in On$
131	109	oien	$⊢ (ran G (⋃ C) \in V \land E We ran G (⋃ C)) \to dom OrdIso (E, ran G (⋃ C)) \approx ran G (⋃ C)$
132	84 108 131	sylancr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to dom OrdIso (E, ran G (⋃ C)) \approx ran G (⋃ C)$
133		fvex	$⊢ R_{1} (⋃ C) \in V$
134	133	f1oen	$⊢ G (⋃ C) : R_{1} (⋃ C) \underset{1-1 onto}{⟶} ran G (⋃ C) \to R_{1} (⋃ C) \approx ran G (⋃ C)$
135		ensym	$⊢ R_{1} (⋃ C) \approx ran G (⋃ C) \to ran G (⋃ C) \approx R_{1} (⋃ C)$
136	102 116 134 135	4syl	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to ran G (⋃ C) \approx R_{1} (⋃ C)$
137		fvex	$⊢ R_{1} (A) \in V$
138	1	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to A \in On$
139	6	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to C \subseteq A$
140	139 101	sseldd	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to ⋃ C \in A$
141		r1ord2	$⊢ A \in On \to (⋃ C \in A \to R_{1} (⋃ C) \subseteq R_{1} (A))$
142	138 140 141	sylc	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to R_{1} (⋃ C) \subseteq R_{1} (A)$
143		ssdomg	$⊢ R_{1} (A) \in V \to (R_{1} (⋃ C) \subseteq R_{1} (A) \to R_{1} (⋃ C) ≼ R_{1} (A))$
144	137 142 143	mpsyl	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to R_{1} (⋃ C) ≼ R_{1} (A)$
145		endomtr	$⊢ (ran G (⋃ C) \approx R_{1} (⋃ C) \land R_{1} (⋃ C) ≼ R_{1} (A)) \to ran G (⋃ C) ≼ R_{1} (A)$
146	136 144 145	syl2anc	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to ran G (⋃ C) ≼ R_{1} (A)$
147		endomtr	$⊢ (dom OrdIso (E, ran G (⋃ C)) \approx ran G (⋃ C) \land ran G (⋃ C) ≼ R_{1} (A)) \to dom OrdIso (E, ran G (⋃ C)) ≼ R_{1} (A)$
148	132 146 147	syl2anc	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to dom OrdIso (E, ran G (⋃ C)) ≼ R_{1} (A)$
149		elharval	$⊢ dom OrdIso (E, ran G (⋃ C)) \in har (R_{1} (A)) \leftrightarrow (dom OrdIso (E, ran G (⋃ C)) \in On \land dom OrdIso (E, ran G (⋃ C)) ≼ R_{1} (A))$
150	130 148 149	sylanbrc	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to dom OrdIso (E, ran G (⋃ C)) \in har (R_{1} (A))$
151		ordelss	$⊢ (Ord har (R_{1} (A)) \land dom OrdIso (E, ran G (⋃ C)) \in har (R_{1} (A))) \to dom OrdIso (E, ran G (⋃ C)) \subseteq har (R_{1} (A))$
152	128 150 151	sylancr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to dom OrdIso (E, ran G (⋃ C)) \subseteq har (R_{1} (A))$
153	126 152	sstrd	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to ran H \subseteq har (R_{1} (A))$
154	82 153	sstrid	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to H [y] \subseteq har (R_{1} (A))$
155		fvex	$⊢ har (R_{1} (A)) \in V$
156	155	elpw2	$⊢ H [y] \in 𝒫 har (R_{1} (A)) \leftrightarrow H [y] \subseteq har (R_{1} (A))$
157	154 156	sylibr	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to H [y] \in 𝒫 har (R_{1} (A))$
158	81 157	ffvelrnd	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to F (H [y]) \in On$
159	78 158	ifclda	$⊢ (φ \land y \in R_{1} (C)) \to if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) \in On$
160	159	ex	$⊢ φ \to (y \in R_{1} (C) \to if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) \in On)$
161		iftrue	$⊢ C = ⋃ C \to if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y)$
162		iftrue	$⊢ C = ⋃ C \to if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) = (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z)$
163	161 162	eqeq12d	$⊢ C = ⋃ C \to (if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) \leftrightarrow (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y) = (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z))$
164	163	adantl	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to (if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) \leftrightarrow (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y) = (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z))$
165	46	ad2antrr	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to suc ⋃ ran ⋃ G [C] \in On$
166		nsuceq0	$⊢ suc ⋃ ran ⋃ G [C] \neq \emptyset$
167	166	a1i	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to suc ⋃ ran ⋃ G [C] \neq \emptyset$
168	48	a1i	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to rank (y) \in On$
169		onsucuni	$⊢ ran ⋃ G [C] \subseteq On \to ran ⋃ G [C] \subseteq suc ⋃ ran ⋃ G [C]$
170	42 169	syl	$⊢ φ \to ran ⋃ G [C] \subseteq suc ⋃ ran ⋃ G [C]$
171	170	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to ran ⋃ G [C] \subseteq suc ⋃ ran ⋃ G [C]$
172	30	ad2antrr	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to C \subseteq On$
173		fnfvima	$⊢ (G Fn On \land C \subseteq On \land suc rank (y) \in C) \to G (suc rank (y)) \in G [C]$
174	8 172 68 173	mp3an2i	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (y)) \in G [C]$
175		elssuni	$⊢ G (suc rank (y)) \in G [C] \to G (suc rank (y)) \subseteq ⋃ G [C]$
176		rnss	$⊢ G (suc rank (y)) \subseteq ⋃ G [C] \to ran G (suc rank (y)) \subseteq ran ⋃ G [C]$
177	174 175 176	3syl	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to ran G (suc rank (y)) \subseteq ran ⋃ G [C]$
178		f1fn	$⊢ G (suc rank (y)) : R_{1} (suc rank (y)) \underset{1-1}{⟶} On \to G (suc rank (y)) Fn R_{1} (suc rank (y))$
179	69 178	syl	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (y)) Fn R_{1} (suc rank (y))$
180		fnfvelrn	$⊢ (G (suc rank (y)) Fn R_{1} (suc rank (y)) \land y \in R_{1} (suc rank (y))) \to G (suc rank (y)) (y) \in ran G (suc rank (y))$
181	179 75 180	syl2anc	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (y)) (y) \in ran G (suc rank (y))$
182	177 181	sseldd	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (y)) (y) \in ran ⋃ G [C]$
183	171 182	sseldd	$⊢ ((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (y)) (y) \in suc ⋃ ran ⋃ G [C]$
184	183	adantlrr	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to G (suc rank (y)) (y) \in suc ⋃ ran ⋃ G [C]$
185		rankon	$⊢ rank (z) \in On$
186	185	a1i	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to rank (z) \in On$
187		eleq1w	$⊢ y = z \to (y \in R_{1} (C) \leftrightarrow z \in R_{1} (C))$
188	187	anbi2d	$⊢ y = z \to ((φ \land y \in R_{1} (C)) \leftrightarrow (φ \land z \in R_{1} (C)))$
189	188	anbi1d	$⊢ y = z \to (((φ \land y \in R_{1} (C)) \land C = ⋃ C) \leftrightarrow ((φ \land z \in R_{1} (C)) \land C = ⋃ C))$
190		fveq2	$⊢ y = z \to rank (y) = rank (z)$
191		suceq	$⊢ rank (y) = rank (z) \to suc rank (y) = suc rank (z)$
192	190 191	syl	$⊢ y = z \to suc rank (y) = suc rank (z)$
193	192	fveq2d	$⊢ y = z \to G (suc rank (y)) = G (suc rank (z))$
194		id	$⊢ y = z \to y = z$
195	193 194	fveq12d	$⊢ y = z \to G (suc rank (y)) (y) = G (suc rank (z)) (z)$
196	195	eleq1d	$⊢ y = z \to (G (suc rank (y)) (y) \in suc ⋃ ran ⋃ G [C] \leftrightarrow G (suc rank (z)) (z) \in suc ⋃ ran ⋃ G [C])$
197	189 196	imbi12d	$⊢ y = z \to ((((φ \land y \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (y)) (y) \in suc ⋃ ran ⋃ G [C]) \leftrightarrow (((φ \land z \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (z)) (z) \in suc ⋃ ran ⋃ G [C]))$
198	197 183	chvarvv	$⊢ ((φ \land z \in R_{1} (C)) \land C = ⋃ C) \to G (suc rank (z)) (z) \in suc ⋃ ran ⋃ G [C]$
199	198	adantlrl	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to G (suc rank (z)) (z) \in suc ⋃ ran ⋃ G [C]$
200		omopth2	$⊢ ((suc ⋃ ran ⋃ G [C] \in On \land suc ⋃ ran ⋃ G [C] \neq \emptyset) \land (rank (y) \in On \land G (suc rank (y)) (y) \in suc ⋃ ran ⋃ G [C]) \land (rank (z) \in On \land G (suc rank (z)) (z) \in suc ⋃ ran ⋃ G [C])) \to ((suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y) = (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z) \leftrightarrow (rank (y) = rank (z) \land G (suc rank (y)) (y) = G (suc rank (z)) (z)))$
201	165 167 168 184 186 199 200	syl222anc	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to ((suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y) = (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z) \leftrightarrow (rank (y) = rank (z) \land G (suc rank (y)) (y) = G (suc rank (z)) (z)))$
202	191	adantl	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to suc rank (y) = suc rank (z)$
203	202	fveq2d	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to G (suc rank (y)) = G (suc rank (z))$
204	203	fveq1d	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to G (suc rank (y)) (z) = G (suc rank (z)) (z)$
205	204	eqeq2d	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to (G (suc rank (y)) (y) = G (suc rank (y)) (z) \leftrightarrow G (suc rank (y)) (y) = G (suc rank (z)) (z))$
206	69	adantlrr	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to G (suc rank (y)) : R_{1} (suc rank (y)) \underset{1-1}{⟶} On$
207	206	adantr	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to G (suc rank (y)) : R_{1} (suc rank (y)) \underset{1-1}{⟶} On$
208	75	adantlrr	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to y \in R_{1} (suc rank (y))$
209	208	adantr	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to y \in R_{1} (suc rank (y))$
210		r1elwf	$⊢ z \in R_{1} (C) \to z \in ⋃ R_{1} [On]$
211		rankidb	$⊢ z \in ⋃ R_{1} [On] \to z \in R_{1} (suc rank (z))$
212	210 211	syl	$⊢ z \in R_{1} (C) \to z \in R_{1} (suc rank (z))$
213	212	ad2antll	$⊢ (φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \to z \in R_{1} (suc rank (z))$
214	213	ad2antrr	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to z \in R_{1} (suc rank (z))$
215	202	fveq2d	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to R_{1} (suc rank (y)) = R_{1} (suc rank (z))$
216	214 215	eleqtrrd	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to z \in R_{1} (suc rank (y))$
217		f1fveq	$⊢ (G (suc rank (y)) : R_{1} (suc rank (y)) \underset{1-1}{⟶} On \land (y \in R_{1} (suc rank (y)) \land z \in R_{1} (suc rank (y)))) \to (G (suc rank (y)) (y) = G (suc rank (y)) (z) \leftrightarrow y = z)$
218	207 209 216 217	syl12anc	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to (G (suc rank (y)) (y) = G (suc rank (y)) (z) \leftrightarrow y = z)$
219	205 218	bitr3d	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to (G (suc rank (y)) (y) = G (suc rank (z)) (z) \leftrightarrow y = z)$
220	219	biimpd	$⊢ (((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \land rank (y) = rank (z)) \to (G (suc rank (y)) (y) = G (suc rank (z)) (z) \to y = z)$
221	220	expimpd	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to ((rank (y) = rank (z) \land G (suc rank (y)) (y) = G (suc rank (z)) (z)) \to y = z)$
222	190 195	jca	$⊢ y = z \to (rank (y) = rank (z) \land G (suc rank (y)) (y) = G (suc rank (z)) (z))$
223	221 222	impbid1	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to ((rank (y) = rank (z) \land G (suc rank (y)) (y) = G (suc rank (z)) (z)) \leftrightarrow y = z)$
224	164 201 223	3bitrd	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land C = ⋃ C) \to (if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) \leftrightarrow y = z)$
225		iffalse	$⊢ \neg C = ⋃ C \to if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = F (H [y])$
226		iffalse	$⊢ \neg C = ⋃ C \to if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) = F (H [z])$
227	225 226	eqeq12d	$⊢ \neg C = ⋃ C \to (if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) \leftrightarrow F (H [y]) = F (H [z]))$
228	227	adantl	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to (if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) \leftrightarrow F (H [y]) = F (H [z]))$
229	2	ad2antrr	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to F : 𝒫 har (R_{1} (A)) \underset{1-1}{⟶} On$
230	157	adantlrr	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to H [y] \in 𝒫 har (R_{1} (A))$
231	188	anbi1d	$⊢ y = z \to (((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \leftrightarrow ((φ \land z \in R_{1} (C)) \land \neg C = ⋃ C))$
232		imaeq2	$⊢ y = z \to H [y] = H [z]$
233	232	eleq1d	$⊢ y = z \to (H [y] \in 𝒫 har (R_{1} (A)) \leftrightarrow H [z] \in 𝒫 har (R_{1} (A)))$
234	231 233	imbi12d	$⊢ y = z \to ((((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to H [y] \in 𝒫 har (R_{1} (A))) \leftrightarrow (((φ \land z \in R_{1} (C)) \land \neg C = ⋃ C) \to H [z] \in 𝒫 har (R_{1} (A))))$
235	234 157	chvarvv	$⊢ ((φ \land z \in R_{1} (C)) \land \neg C = ⋃ C) \to H [z] \in 𝒫 har (R_{1} (A))$
236	235	adantlrl	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to H [z] \in 𝒫 har (R_{1} (A))$
237		f1fveq	$⊢ (F : 𝒫 har (R_{1} (A)) \underset{1-1}{⟶} On \land (H [y] \in 𝒫 har (R_{1} (A)) \land H [z] \in 𝒫 har (R_{1} (A)))) \to (F (H [y]) = F (H [z]) \leftrightarrow H [y] = H [z])$
238	229 230 236 237	syl12anc	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to (F (H [y]) = F (H [z]) \leftrightarrow H [y] = H [z])$
239	123	adantlrr	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to H : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C))$
240		simplrl	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to y \in R_{1} (C)$
241	100	fveq2d	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to R_{1} (C) = R_{1} (suc ⋃ C)$
242		r1suc	$⊢ ⋃ C \in On \to R_{1} (suc ⋃ C) = 𝒫 R_{1} (⋃ C)$
243	93 94 242	3syl	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to R_{1} (suc ⋃ C) = 𝒫 R_{1} (⋃ C)$
244	241 243	eqtrd	$⊢ ((φ \land y \in R_{1} (C)) \land \neg C = ⋃ C) \to R_{1} (C) = 𝒫 R_{1} (⋃ C)$
245	244	adantlrr	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to R_{1} (C) = 𝒫 R_{1} (⋃ C)$
246	240 245	eleqtrd	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to y \in 𝒫 R_{1} (⋃ C)$
247	246	elpwid	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to y \subseteq R_{1} (⋃ C)$
248		simplrr	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to z \in R_{1} (C)$
249	248 245	eleqtrd	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to z \in 𝒫 R_{1} (⋃ C)$
250	249	elpwid	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to z \subseteq R_{1} (⋃ C)$
251		f1imaeq	$⊢ (H : R_{1} (⋃ C) \underset{1-1}{⟶} dom OrdIso (E, ran G (⋃ C)) \land (y \subseteq R_{1} (⋃ C) \land z \subseteq R_{1} (⋃ C))) \to (H [y] = H [z] \leftrightarrow y = z)$
252	239 247 250 251	syl12anc	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to (H [y] = H [z] \leftrightarrow y = z)$
253	228 238 252	3bitrd	$⊢ ((φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \land \neg C = ⋃ C) \to (if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) \leftrightarrow y = z)$
254	224 253	pm2.61dan	$⊢ (φ \land (y \in R_{1} (C) \land z \in R_{1} (C))) \to (if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) \leftrightarrow y = z)$
255	254	ex	$⊢ φ \to ((y \in R_{1} (C) \land z \in R_{1} (C)) \to (if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])) = if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (z)) +_{𝑜} G (suc rank (z)) (z), F (H [z])) \leftrightarrow y = z))$
256	160 255	dom2lem	$⊢ φ \to (y \in R_{1} (C) ⟼ if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y]))) : R_{1} (C) \underset{1-1}{⟶} On$
257	1 2 3 4 5	dfac12lem1	$⊢ φ \to G (C) = (y \in R_{1} (C) ⟼ if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y])))$
258		f1eq1	$⊢ G (C) = (y \in R_{1} (C) ⟼ if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y]))) \to (G (C) : R_{1} (C) \underset{1-1}{⟶} On \leftrightarrow (y \in R_{1} (C) ⟼ if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y]))) : R_{1} (C) \underset{1-1}{⟶} On)$
259	257 258	syl	$⊢ φ \to (G (C) : R_{1} (C) \underset{1-1}{⟶} On \leftrightarrow (y \in R_{1} (C) ⟼ if (C = ⋃ C, (suc ⋃ ran ⋃ G [C] \cdot_{𝑜} rank (y)) +_{𝑜} G (suc rank (y)) (y), F (H [y]))) : R_{1} (C) \underset{1-1}{⟶} On)$
260	256 259	mpbird	$⊢ φ \to G (C) : R_{1} (C) \underset{1-1}{⟶} On$

Metamath Proof Explorer

Theorem dfac12lem2

Proof