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

Metamath Proof Explorer

Theorem dfac12lem2

Proof