cantnflem4

Description: Lemma for cantnf . Complete the induction step of cantnflem3 . (Contributed by Mario Carneiro, 25-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)))\}$
	cantnf.c	$⊢ φ \to C \in (A ↑_{𝑜} B)$
	cantnf.s	$⊢ φ \to C \subseteq ran (A CNF B)$
	cantnf.e	$⊢ φ \to \emptyset \in C$
	cantnf.x	$⊢ X = ⋃ ⋂ \{c \in On \| C \in (A ↑_{𝑜} c)\}$
	cantnf.p	$⊢ P = (ι d \| \exists a \in On \exists b \in (A ↑_{𝑜} X) (d = ⟨a, b⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} a) +_{𝑜} b = C))$
	cantnf.y	$⊢ Y = 1^{st} (P)$
	cantnf.z	$⊢ Z = 2^{nd} (P)$
Assertion	cantnflem4	$⊢ φ \to C \in ran (A CNF 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		cantnf.c	$⊢ φ \to C \in (A ↑_{𝑜} B)$
6		cantnf.s	$⊢ φ \to C \subseteq ran (A CNF B)$
7		cantnf.e	$⊢ φ \to \emptyset \in C$
8		cantnf.x	$⊢ X = ⋃ ⋂ \{c \in On \| C \in (A ↑_{𝑜} c)\}$
9		cantnf.p	$⊢ P = (ι d \| \exists a \in On \exists b \in (A ↑_{𝑜} X) (d = ⟨a, b⟩ \land ((A ↑_{𝑜} X) \cdot_{𝑜} a) +_{𝑜} b = C))$
10		cantnf.y	$⊢ Y = 1^{st} (P)$
11		cantnf.z	$⊢ Z = 2^{nd} (P)$
12	1 2 3 4 5 6 7	cantnflem2	$⊢ φ \to (A \in (On ∖ 2_{𝑜}) \land C \in (On ∖ 1_{𝑜}))$
13		eqid	$⊢ X = X$
14		eqid	$⊢ Y = Y$
15		eqid	$⊢ Z = Z$
16	13 14 15	3pm3.2i	$⊢ (X = X \land Y = Y \land Z = Z)$
17	8 9 10 11	oeeui	$⊢ (A \in (On ∖ 2_{𝑜}) \land C \in (On ∖ 1_{𝑜})) \to (((X \in On \land Y \in (A ∖ 1_{𝑜}) \land Z \in (A ↑_{𝑜} X)) \land ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} Z = C) \leftrightarrow (X = X \land Y = Y \land Z = Z))$
18	16 17	mpbiri	$⊢ (A \in (On ∖ 2_{𝑜}) \land C \in (On ∖ 1_{𝑜})) \to ((X \in On \land Y \in (A ∖ 1_{𝑜}) \land Z \in (A ↑_{𝑜} X)) \land ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} Z = C)$
19	12 18	syl	$⊢ φ \to ((X \in On \land Y \in (A ∖ 1_{𝑜}) \land Z \in (A ↑_{𝑜} X)) \land ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} Z = C)$
20	19	simpld	$⊢ φ \to (X \in On \land Y \in (A ∖ 1_{𝑜}) \land Z \in (A ↑_{𝑜} X))$
21	20	simp1d	$⊢ φ \to X \in On$
22		oecl	$⊢ (A \in On \land X \in On) \to A ↑_{𝑜} X \in On$
23	2 21 22	syl2anc	$⊢ φ \to A ↑_{𝑜} X \in On$
24	20	simp2d	$⊢ φ \to Y \in (A ∖ 1_{𝑜})$
25	24	eldifad	$⊢ φ \to Y \in A$
26		onelon	$⊢ (A \in On \land Y \in A) \to Y \in On$
27	2 25 26	syl2anc	$⊢ φ \to Y \in On$
28		omcl	$⊢ (A ↑_{𝑜} X \in On \land Y \in On) \to (A ↑_{𝑜} X) \cdot_{𝑜} Y \in On$
29	23 27 28	syl2anc	$⊢ φ \to (A ↑_{𝑜} X) \cdot_{𝑜} Y \in On$
30	20	simp3d	$⊢ φ \to Z \in (A ↑_{𝑜} X)$
31		onelon	$⊢ (A ↑_{𝑜} X \in On \land Z \in (A ↑_{𝑜} X)) \to Z \in On$
32	23 30 31	syl2anc	$⊢ φ \to Z \in On$
33		oaword1	$⊢ ((A ↑_{𝑜} X) \cdot_{𝑜} Y \in On \land Z \in On) \to (A ↑_{𝑜} X) \cdot_{𝑜} Y \subseteq ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} Z$
34	29 32 33	syl2anc	$⊢ φ \to (A ↑_{𝑜} X) \cdot_{𝑜} Y \subseteq ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} Z$
35		dif1o	$⊢ Y \in (A ∖ 1_{𝑜}) \leftrightarrow (Y \in A \land Y \neq \emptyset)$
36	35	simprbi	$⊢ Y \in (A ∖ 1_{𝑜}) \to Y \neq \emptyset$
37	24 36	syl	$⊢ φ \to Y \neq \emptyset$
38		on0eln0	$⊢ Y \in On \to (\emptyset \in Y \leftrightarrow Y \neq \emptyset)$
39	27 38	syl	$⊢ φ \to (\emptyset \in Y \leftrightarrow Y \neq \emptyset)$
40	37 39	mpbird	$⊢ φ \to \emptyset \in Y$
41		omword1	$⊢ ((A ↑_{𝑜} X \in On \land Y \in On) \land \emptyset \in Y) \to A ↑_{𝑜} X \subseteq (A ↑_{𝑜} X) \cdot_{𝑜} Y$
42	23 27 40 41	syl21anc	$⊢ φ \to A ↑_{𝑜} X \subseteq (A ↑_{𝑜} X) \cdot_{𝑜} Y$
43	42 30	sseldd	$⊢ φ \to Z \in ((A ↑_{𝑜} X) \cdot_{𝑜} Y)$
44	34 43	sseldd	$⊢ φ \to Z \in (((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} Z)$
45	19	simprd	$⊢ φ \to ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} Z = C$
46	44 45	eleqtrd	$⊢ φ \to Z \in C$
47	6 46	sseldd	$⊢ φ \to Z \in ran (A CNF B)$
48	1 2 3	cantnff	$⊢ φ \to (A CNF B) : S ⟶ A ↑_{𝑜} B$
49		ffn	$⊢ (A CNF B) : S ⟶ A ↑_{𝑜} B \to (A CNF B) Fn S$
50		fvelrnb	$⊢ (A CNF B) Fn S \to (Z \in ran (A CNF B) \leftrightarrow \exists g \in S (A CNF B) (g) = Z)$
51	48 49 50	3syl	$⊢ φ \to (Z \in ran (A CNF B) \leftrightarrow \exists g \in S (A CNF B) (g) = Z)$
52	47 51	mpbid	$⊢ φ \to \exists g \in S (A CNF B) (g) = Z$
53	2	adantr	$⊢ (φ \land (g \in S \land (A CNF B) (g) = Z)) \to A \in On$
54	3	adantr	$⊢ (φ \land (g \in S \land (A CNF B) (g) = Z)) \to B \in On$
55	5	adantr	$⊢ (φ \land (g \in S \land (A CNF B) (g) = Z)) \to C \in (A ↑_{𝑜} B)$
56	6	adantr	$⊢ (φ \land (g \in S \land (A CNF B) (g) = Z)) \to C \subseteq ran (A CNF B)$
57	7	adantr	$⊢ (φ \land (g \in S \land (A CNF B) (g) = Z)) \to \emptyset \in C$
58		simprl	$⊢ (φ \land (g \in S \land (A CNF B) (g) = Z)) \to g \in S$
59		simprr	$⊢ (φ \land (g \in S \land (A CNF B) (g) = Z)) \to (A CNF B) (g) = Z$
60		eqid	$⊢ (t \in B ⟼ if (t = X, Y, g (t))) = (t \in B ⟼ if (t = X, Y, g (t)))$
61	1 53 54 4 55 56 57 8 9 10 11 58 59 60	cantnflem3	$⊢ (φ \land (g \in S \land (A CNF B) (g) = Z)) \to C \in ran (A CNF B)$
62	52 61	rexlimddv	$⊢ φ \to C \in ran (A CNF B)$

Metamath Proof Explorer

Theorem cantnflem4

Proof