cnfcomlem

Description: Lemma for cnfcom . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019)

	Ref	Expression
Hypotheses	cnfcom.s	$⊢ S = dom (ω CNF A)$
	cnfcom.a	$⊢ φ \to A \in On$
	cnfcom.b	$⊢ φ \to B \in (ω ↑_{𝑜} A)$
	cnfcom.f	$⊢ F = {(ω CNF A)}^{-1} (B)$
	cnfcom.g	$⊢ G = OrdIso (E, F supp \emptyset)$
	cnfcom.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
	cnfcom.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
	cnfcom.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
	cnfcom.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
	cnfcom.1	$⊢ φ \to I \in dom G$
	cnfcom.2	$⊢ φ \to O \in (ω ↑_{𝑜} G (I))$
	cnfcom.3	$⊢ φ \to T (I) : H (I) \underset{1-1 onto}{⟶} O$
Assertion	cnfcomlem	$⊢ φ \to T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$

Proof

Step	Hyp	Ref	Expression
1		cnfcom.s	$⊢ S = dom (ω CNF A)$
2		cnfcom.a	$⊢ φ \to A \in On$
3		cnfcom.b	$⊢ φ \to B \in (ω ↑_{𝑜} A)$
4		cnfcom.f	$⊢ F = {(ω CNF A)}^{-1} (B)$
5		cnfcom.g	$⊢ G = OrdIso (E, F supp \emptyset)$
6		cnfcom.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
7		cnfcom.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
8		cnfcom.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
9		cnfcom.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
10		cnfcom.1	$⊢ φ \to I \in dom G$
11		cnfcom.2	$⊢ φ \to O \in (ω ↑_{𝑜} G (I))$
12		cnfcom.3	$⊢ φ \to T (I) : H (I) \underset{1-1 onto}{⟶} O$
13		omelon	$⊢ ω \in On$
14		suppssdm	$⊢ F supp \emptyset \subseteq dom F$
15	13	a1i	$⊢ φ \to ω \in On$
16	1 15 2	cantnff1o	$⊢ φ \to (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A$
17		f1ocnv	$⊢ (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S$
18		f1of	$⊢ {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
19	16 17 18	3syl	$⊢ φ \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
20	19 3	ffvelcdmd	$⊢ φ \to {(ω CNF A)}^{-1} (B) \in S$
21	4 20	eqeltrid	$⊢ φ \to F \in S$
22	1 15 2	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : A ⟶ ω \land {finSupp}_{\emptyset} (F)))$
23	21 22	mpbid	$⊢ φ \to (F : A ⟶ ω \land {finSupp}_{\emptyset} (F))$
24	23	simpld	$⊢ φ \to F : A ⟶ ω$
25	14 24	fssdm	$⊢ φ \to F supp \emptyset \subseteq A$
26	5	oif	$⊢ G : dom G ⟶ F supp \emptyset$
27	26	ffvelcdmi	$⊢ I \in dom G \to G (I) \in {supp}_{\emptyset} (F)$
28	10 27	syl	$⊢ φ \to G (I) \in {supp}_{\emptyset} (F)$
29	25 28	sseldd	$⊢ φ \to G (I) \in A$
30		onelon	$⊢ (A \in On \land G (I) \in A) \to G (I) \in On$
31	2 29 30	syl2anc	$⊢ φ \to G (I) \in On$
32		oecl	$⊢ (ω \in On \land G (I) \in On) \to ω ↑_{𝑜} G (I) \in On$
33	13 31 32	sylancr	$⊢ φ \to ω ↑_{𝑜} G (I) \in On$
34	24 29	ffvelcdmd	$⊢ φ \to F (G (I)) \in ω$
35		nnon	$⊢ F (G (I)) \in ω \to F (G (I)) \in On$
36	34 35	syl	$⊢ φ \to F (G (I)) \in On$
37		omcl	$⊢ (ω ↑_{𝑜} G (I) \in On \land F (G (I)) \in On) \to (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)) \in On$
38	33 36 37	syl2anc	$⊢ φ \to (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)) \in On$
39	1 15 2 5 21	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom G \in ω)$
40	39	simprd	$⊢ φ \to dom G \in ω$
41		elnn	$⊢ (I \in dom G \land dom G \in ω) \to I \in ω$
42	10 40 41	syl2anc	$⊢ φ \to I \in ω$
43	6	cantnfvalf	$⊢ H : ω ⟶ On$
44	43	ffvelcdmi	$⊢ I \in ω \to H (I) \in On$
45	42 44	syl	$⊢ φ \to H (I) \in On$
46		eqid	$⊢ (y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1} = (y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1}$
47	46	oacomf1o	$⊢ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)) \in On \land H (I) \in On) \to ((y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1}) : ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} H (I) \underset{1-1 onto}{⟶} H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)))$
48	38 45 47	syl2anc	$⊢ φ \to ((y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1}) : ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} H (I) \underset{1-1 onto}{⟶} H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)))$
49	7	seqomsuc	$⊢ I \in ω \to T (suc I) = I (k \in V, f \in V ⟼ K) T (I)$
50	42 49	syl	$⊢ φ \to T (suc I) = I (k \in V, f \in V ⟼ K) T (I)$
51		nfcv	$⊢ \underline{Ⅎ} u K$
52		nfcv	$⊢ \underline{Ⅎ} v K$
53		nfcv	$⊢ \underline{Ⅎ} k ((y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y) \cup {(y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)}^{-1})$
54		nfcv	$⊢ \underline{Ⅎ} f ((y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y) \cup {(y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)}^{-1})$
55		oveq2	$⊢ x = y \to dom f +_{𝑜} x = dom f +_{𝑜} y$
56	55	cbvmptv	$⊢ (x \in M ⟼ dom f +_{𝑜} x) = (y \in M ⟼ dom f +_{𝑜} y)$
57		simpl	$⊢ (k = u \land f = v) \to k = u$
58	57	fveq2d	$⊢ (k = u \land f = v) \to G (k) = G (u)$
59	58	oveq2d	$⊢ (k = u \land f = v) \to ω ↑_{𝑜} G (k) = ω ↑_{𝑜} G (u)$
60	58	fveq2d	$⊢ (k = u \land f = v) \to F (G (k)) = F (G (u))$
61	59 60	oveq12d	$⊢ (k = u \land f = v) \to (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k)) = (ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))$
62	8 61	eqtrid	$⊢ (k = u \land f = v) \to M = (ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))$
63		simpr	$⊢ (k = u \land f = v) \to f = v$
64	63	dmeqd	$⊢ (k = u \land f = v) \to dom f = dom v$
65	64	oveq1d	$⊢ (k = u \land f = v) \to dom f +_{𝑜} y = dom v +_{𝑜} y$
66	62 65	mpteq12dv	$⊢ (k = u \land f = v) \to (y \in M ⟼ dom f +_{𝑜} y) = (y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y)$
67	56 66	eqtrid	$⊢ (k = u \land f = v) \to (x \in M ⟼ dom f +_{𝑜} x) = (y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y)$
68		oveq2	$⊢ x = y \to M +_{𝑜} x = M +_{𝑜} y$
69	68	cbvmptv	$⊢ (x \in dom f ⟼ M +_{𝑜} x) = (y \in dom f ⟼ M +_{𝑜} y)$
70	62	oveq1d	$⊢ (k = u \land f = v) \to M +_{𝑜} y = ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y$
71	64 70	mpteq12dv	$⊢ (k = u \land f = v) \to (y \in dom f ⟼ M +_{𝑜} y) = (y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)$
72	69 71	eqtrid	$⊢ (k = u \land f = v) \to (x \in dom f ⟼ M +_{𝑜} x) = (y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)$
73	72	cnveqd	$⊢ (k = u \land f = v) \to {(x \in dom f ⟼ M +_{𝑜} x)}^{-1} = {(y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)}^{-1}$
74	67 73	uneq12d	$⊢ (k = u \land f = v) \to (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1} = (y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y) \cup {(y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)}^{-1}$
75	9 74	eqtrid	$⊢ (k = u \land f = v) \to K = (y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y) \cup {(y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)}^{-1}$
76	51 52 53 54 75	cbvmpo	$⊢ (k \in V, f \in V ⟼ K) = (u \in V, v \in V ⟼ (y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y) \cup {(y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)}^{-1})$
77	76	a1i	$⊢ φ \to (k \in V, f \in V ⟼ K) = (u \in V, v \in V ⟼ (y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y) \cup {(y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)}^{-1})$
78		simprl	$⊢ (φ \land (u = I \land v = T (I))) \to u = I$
79	78	fveq2d	$⊢ (φ \land (u = I \land v = T (I))) \to G (u) = G (I)$
80	79	oveq2d	$⊢ (φ \land (u = I \land v = T (I))) \to ω ↑_{𝑜} G (u) = ω ↑_{𝑜} G (I)$
81	79	fveq2d	$⊢ (φ \land (u = I \land v = T (I))) \to F (G (u)) = F (G (I))$
82	80 81	oveq12d	$⊢ (φ \land (u = I \land v = T (I))) \to (ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u)) = (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$
83		simpr	$⊢ (u = I \land v = T (I)) \to v = T (I)$
84	83	dmeqd	$⊢ (u = I \land v = T (I)) \to dom v = dom T (I)$
85		f1odm	$⊢ T (I) : H (I) \underset{1-1 onto}{⟶} O \to dom T (I) = H (I)$
86	12 85	syl	$⊢ φ \to dom T (I) = H (I)$
87	84 86	sylan9eqr	$⊢ (φ \land (u = I \land v = T (I))) \to dom v = H (I)$
88	87	oveq1d	$⊢ (φ \land (u = I \land v = T (I))) \to dom v +_{𝑜} y = H (I) +_{𝑜} y$
89	82 88	mpteq12dv	$⊢ (φ \land (u = I \land v = T (I))) \to (y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y) = (y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y)$
90	82	oveq1d	$⊢ (φ \land (u = I \land v = T (I))) \to ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y = ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y$
91	87 90	mpteq12dv	$⊢ (φ \land (u = I \land v = T (I))) \to (y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y) = (y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)$
92	91	cnveqd	$⊢ (φ \land (u = I \land v = T (I))) \to {(y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)}^{-1} = {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1}$
93	89 92	uneq12d	$⊢ (φ \land (u = I \land v = T (I))) \to (y \in ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) ⟼ dom v +_{𝑜} y) \cup {(y \in dom v ⟼ ((ω ↑_{𝑜} G (u)) \cdot_{𝑜} F (G (u))) +_{𝑜} y)}^{-1} = (y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1}$
94	10	elexd	$⊢ φ \to I \in V$
95		fvexd	$⊢ φ \to T (I) \in V$
96		ovex	$⊢ (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)) \in V$
97	96	mptex	$⊢ (y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \in V$
98		fvex	$⊢ H (I) \in V$
99	98	mptex	$⊢ (y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y) \in V$
100	99	cnvex	$⊢ {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1} \in V$
101	97 100	unex	$⊢ (y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1} \in V$
102	101	a1i	$⊢ φ \to (y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1} \in V$
103	77 93 94 95 102	ovmpod	$⊢ φ \to I (k \in V, f \in V ⟼ K) T (I) = (y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1}$
104	50 103	eqtrd	$⊢ φ \to T (suc I) = (y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1}$
105	104	f1oeq1d	$⊢ φ \to (T (suc I) : ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} H (I) \underset{1-1 onto}{⟶} H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) \leftrightarrow ((y \in ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) ⟼ H (I) +_{𝑜} y) \cup {(y \in H (I) ⟼ ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} y)}^{-1}) : ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} H (I) \underset{1-1 onto}{⟶} H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))))$
106	48 105	mpbird	$⊢ φ \to T (suc I) : ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} H (I) \underset{1-1 onto}{⟶} H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)))$
107	13	a1i	$⊢ (A \in On \land F \in S) \to ω \in On$
108		simpl	$⊢ (A \in On \land F \in S) \to A \in On$
109		simpr	$⊢ (A \in On \land F \in S) \to F \in S$
110	8	oveq1i	$⊢ M +_{𝑜} z = ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z$
111	110	a1i	$⊢ (k \in V \land z \in V) \to M +_{𝑜} z = ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z$
112	111	mpoeq3ia	$⊢ (k \in V, z \in V ⟼ M +_{𝑜} z) = (k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z)$
113		eqid	$⊢ \emptyset = \emptyset$
114		seqomeq12	$⊢ ((k \in V, z \in V ⟼ M +_{𝑜} z) = (k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) \land \emptyset = \emptyset) \to {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
115	112 113 114	mp2an	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
116	6 115	eqtri	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
117	1 107 108 5 109 116	cantnfsuc	$⊢ ((A \in On \land F \in S) \land I \in ω) \to H (suc I) = ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} H (I)$
118	2 21 42 117	syl21anc	$⊢ φ \to H (suc I) = ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} H (I)$
119	118	f1oeq2d	$⊢ φ \to (T (suc I) : H (suc I) \underset{1-1 onto}{⟶} H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) \leftrightarrow T (suc I) : ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) +_{𝑜} H (I) \underset{1-1 onto}{⟶} H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))))$
120	106 119	mpbird	$⊢ φ \to T (suc I) : H (suc I) \underset{1-1 onto}{⟶} H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)))$
121		sssucid	$⊢ dom G \subseteq suc dom G$
122	121 10	sselid	$⊢ φ \to I \in suc dom G$
123		epelg	$⊢ I \in dom G \to (y E I \leftrightarrow y \in I)$
124	10 123	syl	$⊢ φ \to (y E I \leftrightarrow y \in I)$
125	124	biimpar	$⊢ (φ \land y \in I) \to y E I$
126		ovexd	$⊢ φ \to F supp \emptyset \in V$
127	39	simpld	$⊢ φ \to E We {supp}_{\emptyset} (F)$
128	5	oiiso	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
129	126 127 128	syl2anc	$⊢ φ \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
130	129	adantr	$⊢ (φ \land y \in I) \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
131	5	oicl	$⊢ Ord dom G$
132		ordelss	$⊢ (Ord dom G \land I \in dom G) \to I \subseteq dom G$
133	131 10 132	sylancr	$⊢ φ \to I \subseteq dom G$
134	133	sselda	$⊢ (φ \land y \in I) \to y \in dom G$
135	10	adantr	$⊢ (φ \land y \in I) \to I \in dom G$
136		isorel	$⊢ (G {Isom}_{E, E} (dom G, F supp \emptyset) \land (y \in dom G \land I \in dom G)) \to (y E I \leftrightarrow G (y) E G (I))$
137	130 134 135 136	syl12anc	$⊢ (φ \land y \in I) \to (y E I \leftrightarrow G (y) E G (I))$
138	125 137	mpbid	$⊢ (φ \land y \in I) \to G (y) E G (I)$
139		fvex	$⊢ G (I) \in V$
140	139	epeli	$⊢ G (y) E G (I) \leftrightarrow G (y) \in G (I)$
141	138 140	sylib	$⊢ (φ \land y \in I) \to G (y) \in G (I)$
142	141	ralrimiva	$⊢ φ \to \forall y \in I G (y) \in G (I)$
143		ffun	$⊢ G : dom G ⟶ F supp \emptyset \to Fun G$
144	26 143	ax-mp	$⊢ Fun G$
145		funimass4	$⊢ (Fun G \land I \subseteq dom G) \to (G [I] \subseteq G (I) \leftrightarrow \forall y \in I G (y) \in G (I))$
146	144 133 145	sylancr	$⊢ φ \to (G [I] \subseteq G (I) \leftrightarrow \forall y \in I G (y) \in G (I))$
147	142 146	mpbird	$⊢ φ \to G [I] \subseteq G (I)$
148	13	a1i	$⊢ ((A \in On \land F \in S) \land (I \in suc dom G \land G (I) \in On \land G [I] \subseteq G (I))) \to ω \in On$
149		simpll	$⊢ ((A \in On \land F \in S) \land (I \in suc dom G \land G (I) \in On \land G [I] \subseteq G (I))) \to A \in On$
150		simplr	$⊢ ((A \in On \land F \in S) \land (I \in suc dom G \land G (I) \in On \land G [I] \subseteq G (I))) \to F \in S$
151		peano1	$⊢ \emptyset \in ω$
152	151	a1i	$⊢ ((A \in On \land F \in S) \land (I \in suc dom G \land G (I) \in On \land G [I] \subseteq G (I))) \to \emptyset \in ω$
153		simpr1	$⊢ ((A \in On \land F \in S) \land (I \in suc dom G \land G (I) \in On \land G [I] \subseteq G (I))) \to I \in suc dom G$
154		simpr2	$⊢ ((A \in On \land F \in S) \land (I \in suc dom G \land G (I) \in On \land G [I] \subseteq G (I))) \to G (I) \in On$
155		simpr3	$⊢ ((A \in On \land F \in S) \land (I \in suc dom G \land G (I) \in On \land G [I] \subseteq G (I))) \to G [I] \subseteq G (I)$
156	1 148 149 5 150 116 152 153 154 155	cantnflt	$⊢ ((A \in On \land F \in S) \land (I \in suc dom G \land G (I) \in On \land G [I] \subseteq G (I))) \to H (I) \in (ω ↑_{𝑜} G (I))$
157	2 21 122 31 147 156	syl23anc	$⊢ φ \to H (I) \in (ω ↑_{𝑜} G (I))$
158	24	ffnd	$⊢ φ \to F Fn A$
159		0ex	$⊢ \emptyset \in V$
160	159	a1i	$⊢ φ \to \emptyset \in V$
161		elsuppfn	$⊢ (F Fn A \land A \in On \land \emptyset \in V) \to (G (I) \in {supp}_{\emptyset} (F) \leftrightarrow (G (I) \in A \land F (G (I)) \neq \emptyset))$
162	158 2 160 161	syl3anc	$⊢ φ \to (G (I) \in {supp}_{\emptyset} (F) \leftrightarrow (G (I) \in A \land F (G (I)) \neq \emptyset))$
163		simpr	$⊢ (G (I) \in A \land F (G (I)) \neq \emptyset) \to F (G (I)) \neq \emptyset$
164	162 163	biimtrdi	$⊢ φ \to (G (I) \in {supp}_{\emptyset} (F) \to F (G (I)) \neq \emptyset)$
165	28 164	mpd	$⊢ φ \to F (G (I)) \neq \emptyset$
166		on0eln0	$⊢ F (G (I)) \in On \to (\emptyset \in F (G (I)) \leftrightarrow F (G (I)) \neq \emptyset)$
167	36 166	syl	$⊢ φ \to (\emptyset \in F (G (I)) \leftrightarrow F (G (I)) \neq \emptyset)$
168	165 167	mpbird	$⊢ φ \to \emptyset \in F (G (I))$
169		omword1	$⊢ ((ω ↑_{𝑜} G (I) \in On \land F (G (I)) \in On) \land \emptyset \in F (G (I))) \to ω ↑_{𝑜} G (I) \subseteq (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$
170	33 36 168 169	syl21anc	$⊢ φ \to ω ↑_{𝑜} G (I) \subseteq (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$
171		oaabs2	$⊢ ((H (I) \in (ω ↑_{𝑜} G (I)) \land (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)) \in On) \land ω ↑_{𝑜} G (I) \subseteq (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) \to H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) = (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$
172	157 38 170 171	syl21anc	$⊢ φ \to H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) = (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$
173	172	f1oeq3d	$⊢ φ \to (T (suc I) : H (suc I) \underset{1-1 onto}{⟶} H (I) +_{𝑜} ((ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))) \leftrightarrow T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I)))$
174	120 173	mpbid	$⊢ φ \to T (suc I) : H (suc I) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (I)) \cdot_{𝑜} F (G (I))$

Metamath Proof Explorer

Theorem cnfcomlem

Proof