cantnflem2

	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$
Assertion	cantnflem2	$⊢ φ \to (A \in (On ∖ 2_{𝑜}) \land C \in (On ∖ 1_{𝑜}))$

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		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
9	2 3 8	syl2anc	$⊢ φ \to A ↑_{𝑜} B \in On$
10		onelon	$⊢ (A ↑_{𝑜} B \in On \land C \in (A ↑_{𝑜} B)) \to C \in On$
11	9 5 10	syl2anc	$⊢ φ \to C \in On$
12		ondif1	$⊢ C \in (On ∖ 1_{𝑜}) \leftrightarrow (C \in On \land \emptyset \in C)$
13	11 7 12	sylanbrc	$⊢ φ \to C \in (On ∖ 1_{𝑜})$
14	13	eldifbd	$⊢ φ \to \neg C \in 1_{𝑜}$
15		ssel	$⊢ A ↑_{𝑜} B \subseteq 1_{𝑜} \to (C \in (A ↑_{𝑜} B) \to C \in 1_{𝑜})$
16	5 15	syl5com	$⊢ φ \to (A ↑_{𝑜} B \subseteq 1_{𝑜} \to C \in 1_{𝑜})$
17	14 16	mtod	$⊢ φ \to \neg A ↑_{𝑜} B \subseteq 1_{𝑜}$
18		oe0m	$⊢ B \in On \to \emptyset ↑_{𝑜} B = 1_{𝑜} ∖ B$
19	3 18	syl	$⊢ φ \to \emptyset ↑_{𝑜} B = 1_{𝑜} ∖ B$
20		difss	$⊢ 1_{𝑜} ∖ B \subseteq 1_{𝑜}$
21	19 20	eqsstrdi	$⊢ φ \to \emptyset ↑_{𝑜} B \subseteq 1_{𝑜}$
22		oveq1	$⊢ A = \emptyset \to A ↑_{𝑜} B = \emptyset ↑_{𝑜} B$
23	22	sseq1d	$⊢ A = \emptyset \to (A ↑_{𝑜} B \subseteq 1_{𝑜} \leftrightarrow \emptyset ↑_{𝑜} B \subseteq 1_{𝑜})$
24	21 23	syl5ibrcom	$⊢ φ \to (A = \emptyset \to A ↑_{𝑜} B \subseteq 1_{𝑜})$
25		oe1m	$⊢ B \in On \to 1_{𝑜} ↑_{𝑜} B = 1_{𝑜}$
26		eqimss	$⊢ 1_{𝑜} ↑_{𝑜} B = 1_{𝑜} \to 1_{𝑜} ↑_{𝑜} B \subseteq 1_{𝑜}$
27	3 25 26	3syl	$⊢ φ \to 1_{𝑜} ↑_{𝑜} B \subseteq 1_{𝑜}$
28		oveq1	$⊢ A = 1_{𝑜} \to A ↑_{𝑜} B = 1_{𝑜} ↑_{𝑜} B$
29	28	sseq1d	$⊢ A = 1_{𝑜} \to (A ↑_{𝑜} B \subseteq 1_{𝑜} \leftrightarrow 1_{𝑜} ↑_{𝑜} B \subseteq 1_{𝑜})$
30	27 29	syl5ibrcom	$⊢ φ \to (A = 1_{𝑜} \to A ↑_{𝑜} B \subseteq 1_{𝑜})$
31	24 30	jaod	$⊢ φ \to ((A = \emptyset \lor A = 1_{𝑜}) \to A ↑_{𝑜} B \subseteq 1_{𝑜})$
32	17 31	mtod	$⊢ φ \to \neg (A = \emptyset \lor A = 1_{𝑜})$
33		elpri	$⊢ A \in \{\emptyset, 1_{𝑜}\} \to (A = \emptyset \lor A = 1_{𝑜})$
34		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
35	33 34	eleq2s	$⊢ A \in 2_{𝑜} \to (A = \emptyset \lor A = 1_{𝑜})$
36	32 35	nsyl	$⊢ φ \to \neg A \in 2_{𝑜}$
37	2 36	eldifd	$⊢ φ \to A \in (On ∖ 2_{𝑜})$
38	37 13	jca	$⊢ φ \to (A \in (On ∖ 2_{𝑜}) \land C \in (On ∖ 1_{𝑜}))$

Metamath Proof Explorer

Theorem cantnflem2

Proof