cantnf

Description: The Cantor Normal Form theorem. The function ( A CNF B ) , which maps a finitely supported function from B to A to the sum ( ( A ^o f ( a 1 ) ) o. a 1 ) +o ( ( A ^o f ( a 2 ) ) o. a 2 ) +o ... over all indices a < B such that f ( a ) is nonzero, is an order isomorphism from the ordering T of finitely supported functions to the set ( A ^o B ) under the natural order. Setting A = _om and letting B be arbitrarily large, the surjectivity of this function implies that every ordinal has a Cantor normal form (and injectivity, together with coherence cantnfres , implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
Assertion	cantnf	$⊢ φ \to (A CNF B) {Isom}_{T, E} (S, A ↑_{𝑜} B)$

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	$⊢ S = dom (A CNF B)$
2		cantnfs.a	$⊢ φ \to A \in On$
3		cantnfs.b	$⊢ φ \to B \in On$
4		oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
5	1 2 3 4	oemapso	$⊢ φ \to T Or S$
6		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
7	2 3 6	syl2anc	$⊢ φ \to A ↑_{𝑜} B \in On$
8		eloni	$⊢ A ↑_{𝑜} B \in On \to Ord (A ↑_{𝑜} B)$
9	7 8	syl	$⊢ φ \to Ord (A ↑_{𝑜} B)$
10		ordwe	$⊢ Ord (A ↑_{𝑜} B) \to E We (A ↑_{𝑜} B)$
11		weso	$⊢ E We (A ↑_{𝑜} B) \to E Or (A ↑_{𝑜} B)$
12		sopo	$⊢ E Or (A ↑_{𝑜} B) \to E Po (A ↑_{𝑜} B)$
13	9 10 11 12	4syl	$⊢ φ \to E Po (A ↑_{𝑜} B)$
14	1 2 3	cantnff	$⊢ φ \to (A CNF B) : S ⟶ A ↑_{𝑜} B$
15	14	frnd	$⊢ φ \to ran (A CNF B) \subseteq A ↑_{𝑜} B$
16		onss	$⊢ A ↑_{𝑜} B \in On \to A ↑_{𝑜} B \subseteq On$
17	7 16	syl	$⊢ φ \to A ↑_{𝑜} B \subseteq On$
18	17	sseld	$⊢ φ \to (t \in (A ↑_{𝑜} B) \to t \in On)$
19		eleq1w	$⊢ t = y \to (t \in (A ↑_{𝑜} B) \leftrightarrow y \in (A ↑_{𝑜} B))$
20		eleq1w	$⊢ t = y \to (t \in ran (A CNF B) \leftrightarrow y \in ran (A CNF B))$
21	19 20	imbi12d	$⊢ t = y \to ((t \in (A ↑_{𝑜} B) \to t \in ran (A CNF B)) \leftrightarrow (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B)))$
22	21	imbi2d	$⊢ t = y \to ((φ \to (t \in (A ↑_{𝑜} B) \to t \in ran (A CNF B))) \leftrightarrow (φ \to (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B))))$
23		r19.21v	$⊢ \forall y \in t (φ \to (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B))) \leftrightarrow (φ \to \forall y \in t (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B)))$
24		ordelss	$⊢ (Ord (A ↑_{𝑜} B) \land t \in (A ↑_{𝑜} B)) \to t \subseteq A ↑_{𝑜} B$
25	9 24	sylan	$⊢ (φ \land t \in (A ↑_{𝑜} B)) \to t \subseteq A ↑_{𝑜} B$
26	25	sselda	$⊢ ((φ \land t \in (A ↑_{𝑜} B)) \land y \in t) \to y \in (A ↑_{𝑜} B)$
27		pm5.5	$⊢ y \in (A ↑_{𝑜} B) \to ((y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B)) \leftrightarrow y \in ran (A CNF B))$
28	26 27	syl	$⊢ ((φ \land t \in (A ↑_{𝑜} B)) \land y \in t) \to ((y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B)) \leftrightarrow y \in ran (A CNF B))$
29	28	ralbidva	$⊢ (φ \land t \in (A ↑_{𝑜} B)) \to (\forall y \in t (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B)) \leftrightarrow \forall y \in t y \in ran (A CNF B))$
30		dfss3	$⊢ t \subseteq ran (A CNF B) \leftrightarrow \forall y \in t y \in ran (A CNF B)$
31	29 30	bitr4di	$⊢ (φ \land t \in (A ↑_{𝑜} B)) \to (\forall y \in t (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B)) \leftrightarrow t \subseteq ran (A CNF B))$
32		eleq1	$⊢ t = \emptyset \to (t \in ran (A CNF B) \leftrightarrow \emptyset \in ran (A CNF B))$
33	2	adantr	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to A \in On$
34	33	adantr	$⊢ ((φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \land t \neq \emptyset) \to A \in On$
35	3	adantr	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to B \in On$
36	35	adantr	$⊢ ((φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \land t \neq \emptyset) \to B \in On$
37		simplrl	$⊢ ((φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \land t \neq \emptyset) \to t \in (A ↑_{𝑜} B)$
38		simplrr	$⊢ ((φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \land t \neq \emptyset) \to t \subseteq ran (A CNF B)$
39	7	adantr	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to A ↑_{𝑜} B \in On$
40		simprl	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to t \in (A ↑_{𝑜} B)$
41		onelon	$⊢ (A ↑_{𝑜} B \in On \land t \in (A ↑_{𝑜} B)) \to t \in On$
42	39 40 41	syl2anc	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to t \in On$
43		on0eln0	$⊢ t \in On \to (\emptyset \in t \leftrightarrow t \neq \emptyset)$
44	42 43	syl	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (\emptyset \in t \leftrightarrow t \neq \emptyset)$
45	44	biimpar	$⊢ ((φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \land t \neq \emptyset) \to \emptyset \in t$
46		eqid	$⊢ ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\} = ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}$
47		eqid	$⊢ (ι d \| \exists a \in On \exists b \in (A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) (d = ⟨a, b⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) \cdot_{𝑜} a) +_{𝑜} b = t)) = (ι d \| \exists a \in On \exists b \in (A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) (d = ⟨a, b⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) \cdot_{𝑜} a) +_{𝑜} b = t))$
48		eqid	$⊢ 1^{st} ((ι d \| \exists a \in On \exists b \in (A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) (d = ⟨a, b⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) \cdot_{𝑜} a) +_{𝑜} b = t))) = 1^{st} ((ι d \| \exists a \in On \exists b \in (A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) (d = ⟨a, b⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) \cdot_{𝑜} a) +_{𝑜} b = t)))$
49		eqid	$⊢ 2^{nd} ((ι d \| \exists a \in On \exists b \in (A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) (d = ⟨a, b⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) \cdot_{𝑜} a) +_{𝑜} b = t))) = 2^{nd} ((ι d \| \exists a \in On \exists b \in (A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) (d = ⟨a, b⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{c \in On \| t \in (A ↑_{𝑜} c)\}) \cdot_{𝑜} a) +_{𝑜} b = t)))$
50	1 34 36 4 37 38 45 46 47 48 49	cantnflem4	$⊢ ((φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \land t \neq \emptyset) \to t \in ran (A CNF B)$
51		fczsupp0	$⊢ (B \times \{\emptyset\}) supp \emptyset = \emptyset$
52	51	eqcomi	$⊢ \emptyset = (B \times \{\emptyset\}) supp \emptyset$
53		oieq2	$⊢ \emptyset = (B \times \{\emptyset\}) supp \emptyset \to OrdIso (E, \emptyset) = OrdIso (E, (B \times \{\emptyset\}) supp \emptyset)$
54	52 53	ax-mp	$⊢ OrdIso (E, \emptyset) = OrdIso (E, (B \times \{\emptyset\}) supp \emptyset)$
55		ne0i	$⊢ t \in (A ↑_{𝑜} B) \to A ↑_{𝑜} B \neq \emptyset$
56	55	ad2antrl	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to A ↑_{𝑜} B \neq \emptyset$
57		oveq1	$⊢ A = \emptyset \to A ↑_{𝑜} B = \emptyset ↑_{𝑜} B$
58	57	neeq1d	$⊢ A = \emptyset \to (A ↑_{𝑜} B \neq \emptyset \leftrightarrow \emptyset ↑_{𝑜} B \neq \emptyset)$
59	56 58	syl5ibcom	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (A = \emptyset \to \emptyset ↑_{𝑜} B \neq \emptyset)$
60	59	necon2d	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (\emptyset ↑_{𝑜} B = \emptyset \to A \neq \emptyset)$
61		on0eln0	$⊢ B \in On \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
62		oe0m1	$⊢ B \in On \to (\emptyset \in B \leftrightarrow \emptyset ↑_{𝑜} B = \emptyset)$
63	61 62	bitr3d	$⊢ B \in On \to (B \neq \emptyset \leftrightarrow \emptyset ↑_{𝑜} B = \emptyset)$
64	35 63	syl	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (B \neq \emptyset \leftrightarrow \emptyset ↑_{𝑜} B = \emptyset)$
65		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
66	33 65	syl	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
67	60 64 66	3imtr4d	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (B \neq \emptyset \to \emptyset \in A)$
68		ne0i	$⊢ y \in B \to B \neq \emptyset$
69	67 68	impel	$⊢ ((φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \land y \in B) \to \emptyset \in A$
70		fconstmpt	$⊢ B \times \{\emptyset\} = (y \in B ⟼ \emptyset)$
71	69 70	fmptd	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (B \times \{\emptyset\}) : B ⟶ A$
72		0ex	$⊢ \emptyset \in V$
73	72	a1i	$⊢ φ \to \emptyset \in V$
74	3 73	fczfsuppd	$⊢ φ \to {finSupp}_{\emptyset} ((B \times \{\emptyset\}))$
75	74	adantr	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to {finSupp}_{\emptyset} ((B \times \{\emptyset\}))$
76	1 2 3	cantnfs	$⊢ φ \to (B \times \{\emptyset\} \in S \leftrightarrow ((B \times \{\emptyset\}) : B ⟶ A \land {finSupp}_{\emptyset} ((B \times \{\emptyset\}))))$
77	76	adantr	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (B \times \{\emptyset\} \in S \leftrightarrow ((B \times \{\emptyset\}) : B ⟶ A \land {finSupp}_{\emptyset} ((B \times \{\emptyset\}))))$
78	71 75 77	mpbir2and	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to B \times \{\emptyset\} \in S$
79		eqid	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, \emptyset) (k)) \cdot_{𝑜} (B \times \{\emptyset\}) (OrdIso (E, \emptyset) (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, \emptyset) (k)) \cdot_{𝑜} (B \times \{\emptyset\}) (OrdIso (E, \emptyset) (k))) +_{𝑜} z), \emptyset)$
80	1 33 35 54 78 79	cantnfval	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (A CNF B) (B \times \{\emptyset\}) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, \emptyset) (k)) \cdot_{𝑜} (B \times \{\emptyset\}) (OrdIso (E, \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, \emptyset))$
81		we0	$⊢ E We \emptyset$
82		eqid	$⊢ OrdIso (E, \emptyset) = OrdIso (E, \emptyset)$
83	82	oien	$⊢ (\emptyset \in V \land E We \emptyset) \to dom OrdIso (E, \emptyset) \approx \emptyset$
84	72 81 83	mp2an	$⊢ dom OrdIso (E, \emptyset) \approx \emptyset$
85		en0	$⊢ dom OrdIso (E, \emptyset) \approx \emptyset \leftrightarrow dom OrdIso (E, \emptyset) = \emptyset$
86	84 85	mpbi	$⊢ dom OrdIso (E, \emptyset) = \emptyset$
87	86	fveq2i	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, \emptyset) (k)) \cdot_{𝑜} (B \times \{\emptyset\}) (OrdIso (E, \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, \emptyset)) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, \emptyset) (k)) \cdot_{𝑜} (B \times \{\emptyset\}) (OrdIso (E, \emptyset) (k))) +_{𝑜} z), \emptyset) (\emptyset)$
88	79	seqom0g	$⊢ \emptyset \in V \to {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, \emptyset) (k)) \cdot_{𝑜} (B \times \{\emptyset\}) (OrdIso (E, \emptyset) (k))) +_{𝑜} z), \emptyset) (\emptyset) = \emptyset$
89	72 88	ax-mp	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, \emptyset) (k)) \cdot_{𝑜} (B \times \{\emptyset\}) (OrdIso (E, \emptyset) (k))) +_{𝑜} z), \emptyset) (\emptyset) = \emptyset$
90	87 89	eqtri	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, \emptyset) (k)) \cdot_{𝑜} (B \times \{\emptyset\}) (OrdIso (E, \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, \emptyset)) = \emptyset$
91	80 90	eqtrdi	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (A CNF B) (B \times \{\emptyset\}) = \emptyset$
92	14	adantr	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (A CNF B) : S ⟶ A ↑_{𝑜} B$
93	92	ffnd	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (A CNF B) Fn S$
94		fnfvelrn	$⊢ ((A CNF B) Fn S \land B \times \{\emptyset\} \in S) \to (A CNF B) (B \times \{\emptyset\}) \in ran (A CNF B)$
95	93 78 94	syl2anc	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to (A CNF B) (B \times \{\emptyset\}) \in ran (A CNF B)$
96	91 95	eqeltrrd	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to \emptyset \in ran (A CNF B)$
97	32 50 96	pm2.61ne	$⊢ (φ \land (t \in (A ↑_{𝑜} B) \land t \subseteq ran (A CNF B))) \to t \in ran (A CNF B)$
98	97	expr	$⊢ (φ \land t \in (A ↑_{𝑜} B)) \to (t \subseteq ran (A CNF B) \to t \in ran (A CNF B))$
99	31 98	sylbid	$⊢ (φ \land t \in (A ↑_{𝑜} B)) \to (\forall y \in t (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B)) \to t \in ran (A CNF B))$
100	99	ex	$⊢ φ \to (t \in (A ↑_{𝑜} B) \to (\forall y \in t (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B)) \to t \in ran (A CNF B)))$
101	100	com23	$⊢ φ \to (\forall y \in t (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B)) \to (t \in (A ↑_{𝑜} B) \to t \in ran (A CNF B)))$
102	101	a2i	$⊢ (φ \to \forall y \in t (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B))) \to (φ \to (t \in (A ↑_{𝑜} B) \to t \in ran (A CNF B)))$
103	102	a1i	$⊢ t \in On \to ((φ \to \forall y \in t (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B))) \to (φ \to (t \in (A ↑_{𝑜} B) \to t \in ran (A CNF B))))$
104	23 103	syl5bi	$⊢ t \in On \to (\forall y \in t (φ \to (y \in (A ↑_{𝑜} B) \to y \in ran (A CNF B))) \to (φ \to (t \in (A ↑_{𝑜} B) \to t \in ran (A CNF B))))$
105	22 104	tfis2	$⊢ t \in On \to (φ \to (t \in (A ↑_{𝑜} B) \to t \in ran (A CNF B)))$
106	105	com3l	$⊢ φ \to (t \in (A ↑_{𝑜} B) \to (t \in On \to t \in ran (A CNF B)))$
107	18 106	mpdd	$⊢ φ \to (t \in (A ↑_{𝑜} B) \to t \in ran (A CNF B))$
108	107	ssrdv	$⊢ φ \to A ↑_{𝑜} B \subseteq ran (A CNF B)$
109	15 108	eqssd	$⊢ φ \to ran (A CNF B) = A ↑_{𝑜} B$
110		dffo2	$⊢ (A CNF B) : S \underset{onto}{⟶} A ↑_{𝑜} B \leftrightarrow ((A CNF B) : S ⟶ A ↑_{𝑜} B \land ran (A CNF B) = A ↑_{𝑜} B)$
111	14 109 110	sylanbrc	$⊢ φ \to (A CNF B) : S \underset{onto}{⟶} A ↑_{𝑜} B$
112	2	adantr	$⊢ (φ \land ((f \in S \land g \in S) \land f T g)) \to A \in On$
113	3	adantr	$⊢ (φ \land ((f \in S \land g \in S) \land f T g)) \to B \in On$
114		fveq2	$⊢ z = t \to x (z) = x (t)$
115		fveq2	$⊢ z = t \to y (z) = y (t)$
116	114 115	eleq12d	$⊢ z = t \to (x (z) \in y (z) \leftrightarrow x (t) \in y (t))$
117		eleq1w	$⊢ z = t \to (z \in w \leftrightarrow t \in w)$
118	117	imbi1d	$⊢ z = t \to ((z \in w \to x (w) = y (w)) \leftrightarrow (t \in w \to x (w) = y (w)))$
119	118	ralbidv	$⊢ z = t \to (\forall w \in B (z \in w \to x (w) = y (w)) \leftrightarrow \forall w \in B (t \in w \to x (w) = y (w)))$
120	116 119	anbi12d	$⊢ z = t \to ((x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w))) \leftrightarrow (x (t) \in y (t) \land \forall w \in B (t \in w \to x (w) = y (w))))$
121	120	cbvrexvw	$⊢ \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w))) \leftrightarrow \exists t \in B (x (t) \in y (t) \land \forall w \in B (t \in w \to x (w) = y (w)))$
122		fveq1	$⊢ x = u \to x (t) = u (t)$
123		fveq1	$⊢ y = v \to y (t) = v (t)$
124		eleq12	$⊢ (x (t) = u (t) \land y (t) = v (t)) \to (x (t) \in y (t) \leftrightarrow u (t) \in v (t))$
125	122 123 124	syl2an	$⊢ (x = u \land y = v) \to (x (t) \in y (t) \leftrightarrow u (t) \in v (t))$
126		fveq1	$⊢ x = u \to x (w) = u (w)$
127		fveq1	$⊢ y = v \to y (w) = v (w)$
128	126 127	eqeqan12d	$⊢ (x = u \land y = v) \to (x (w) = y (w) \leftrightarrow u (w) = v (w))$
129	128	imbi2d	$⊢ (x = u \land y = v) \to ((t \in w \to x (w) = y (w)) \leftrightarrow (t \in w \to u (w) = v (w)))$
130	129	ralbidv	$⊢ (x = u \land y = v) \to (\forall w \in B (t \in w \to x (w) = y (w)) \leftrightarrow \forall w \in B (t \in w \to u (w) = v (w)))$
131	125 130	anbi12d	$⊢ (x = u \land y = v) \to ((x (t) \in y (t) \land \forall w \in B (t \in w \to x (w) = y (w))) \leftrightarrow (u (t) \in v (t) \land \forall w \in B (t \in w \to u (w) = v (w))))$
132	131	rexbidv	$⊢ (x = u \land y = v) \to (\exists t \in B (x (t) \in y (t) \land \forall w \in B (t \in w \to x (w) = y (w))) \leftrightarrow \exists t \in B (u (t) \in v (t) \land \forall w \in B (t \in w \to u (w) = v (w))))$
133	121 132	syl5bb	$⊢ (x = u \land y = v) \to (\exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w))) \leftrightarrow \exists t \in B (u (t) \in v (t) \land \forall w \in B (t \in w \to u (w) = v (w))))$
134	133	cbvopabv	$⊢ \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\} = \{⟨u, v⟩ \| \exists t \in B (u (t) \in v (t) \land \forall w \in B (t \in w \to u (w) = v (w)))\}$
135	4 134	eqtri	$⊢ T = \{⟨u, v⟩ \| \exists t \in B (u (t) \in v (t) \land \forall w \in B (t \in w \to u (w) = v (w)))\}$
136		simprll	$⊢ (φ \land ((f \in S \land g \in S) \land f T g)) \to f \in S$
137		simprlr	$⊢ (φ \land ((f \in S \land g \in S) \land f T g)) \to g \in S$
138		simprr	$⊢ (φ \land ((f \in S \land g \in S) \land f T g)) \to f T g$
139		eqid	$⊢ ⋃ \{c \in B \| f (c) \in g (c)\} = ⋃ \{c \in B \| f (c) \in g (c)\}$
140		eqid	$⊢ OrdIso (E, g supp \emptyset) = OrdIso (E, g supp \emptyset)$
141		eqid	$⊢ {seq}_{ω} ((k \in V, t \in V ⟼ ((A ↑_{𝑜} OrdIso (E, g supp \emptyset) (k)) \cdot_{𝑜} g (OrdIso (E, g supp \emptyset) (k))) +_{𝑜} t), \emptyset) = {seq}_{ω} ((k \in V, t \in V ⟼ ((A ↑_{𝑜} OrdIso (E, g supp \emptyset) (k)) \cdot_{𝑜} g (OrdIso (E, g supp \emptyset) (k))) +_{𝑜} t), \emptyset)$
142	1 112 113 135 136 137 138 139 140 141	cantnflem1	$⊢ (φ \land ((f \in S \land g \in S) \land f T g)) \to (A CNF B) (f) \in (A CNF B) (g)$
143		fvex	$⊢ (A CNF B) (g) \in V$
144	143	epeli	$⊢ (A CNF B) (f) E (A CNF B) (g) \leftrightarrow (A CNF B) (f) \in (A CNF B) (g)$
145	142 144	sylibr	$⊢ (φ \land ((f \in S \land g \in S) \land f T g)) \to (A CNF B) (f) E (A CNF B) (g)$
146	145	expr	$⊢ (φ \land (f \in S \land g \in S)) \to (f T g \to (A CNF B) (f) E (A CNF B) (g))$
147	146	ralrimivva	$⊢ φ \to \forall f \in S \forall g \in S (f T g \to (A CNF B) (f) E (A CNF B) (g))$
148		soisoi	$⊢ ((T Or S \land E Po (A ↑_{𝑜} B)) \land ((A CNF B) : S \underset{onto}{⟶} A ↑_{𝑜} B \land \forall f \in S \forall g \in S (f T g \to (A CNF B) (f) E (A CNF B) (g)))) \to (A CNF B) {Isom}_{T, E} (S, A ↑_{𝑜} B)$
149	5 13 111 147 148	syl22anc	$⊢ φ \to (A CNF B) {Isom}_{T, E} (S, A ↑_{𝑜} B)$

Metamath Proof Explorer

Theorem cantnf

Proof