cantnflem1c

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019) (Proof shortened by AV, 4-Apr-2020)

	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)))\}$
	oemapval.f	$⊢ φ \to F \in S$
	oemapval.g	$⊢ φ \to G \in S$
	oemapvali.r	$⊢ φ \to F T G$
	oemapvali.x	$⊢ X = ⋃ \{c \in B \| F (c) \in G (c)\}$
	cantnflem1.o	$⊢ O = OrdIso (E, G supp \emptyset)$
Assertion	cantnflem1c	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to x \in {supp}_{\emptyset} (G)$

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		oemapval.f	$⊢ φ \to F \in S$
6		oemapval.g	$⊢ φ \to G \in S$
7		oemapvali.r	$⊢ φ \to F T G$
8		oemapvali.x	$⊢ X = ⋃ \{c \in B \| F (c) \in G (c)\}$
9		cantnflem1.o	$⊢ O = OrdIso (E, G supp \emptyset)$
10	3	ad3antrrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to B \in On$
11		simplr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to x \in B$
12	1 2 3	cantnfs	$⊢ φ \to (G \in S \leftrightarrow (G : B ⟶ A \land {finSupp}_{\emptyset} (G)))$
13	6 12	mpbid	$⊢ φ \to (G : B ⟶ A \land {finSupp}_{\emptyset} (G))$
14	13	simpld	$⊢ φ \to G : B ⟶ A$
15	14	ffnd	$⊢ φ \to G Fn B$
16	15	ad3antrrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to G Fn B$
17	1 2 3 4 5 6 7 8 9	cantnflem1b	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to X \subseteq O (u)$
18	17	ad2antrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to X \subseteq O (u)$
19		simprr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to O (u) \in x$
20	1 2 3 4 5 6 7 8	oemapvali	$⊢ φ \to (X \in B \land F (X) \in G (X) \land \forall w \in B (X \in w \to F (w) = G (w)))$
21	20	simp1d	$⊢ φ \to X \in B$
22		onelon	$⊢ (B \in On \land X \in B) \to X \in On$
23	3 21 22	syl2anc	$⊢ φ \to X \in On$
24	23	ad3antrrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to X \in On$
25		onss	$⊢ B \in On \to B \subseteq On$
26	3 25	syl	$⊢ φ \to B \subseteq On$
27	26	sselda	$⊢ (φ \land x \in B) \to x \in On$
28	27	ad4ant13	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to x \in On$
29		ontr2	$⊢ (X \in On \land x \in On) \to ((X \subseteq O (u) \land O (u) \in x) \to X \in x)$
30	24 28 29	syl2anc	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to ((X \subseteq O (u) \land O (u) \in x) \to X \in x)$
31	18 19 30	mp2and	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to X \in x$
32		eleq2w	$⊢ w = x \to (X \in w \leftrightarrow X \in x)$
33		fveq2	$⊢ w = x \to F (w) = F (x)$
34		fveq2	$⊢ w = x \to G (w) = G (x)$
35	33 34	eqeq12d	$⊢ w = x \to (F (w) = G (w) \leftrightarrow F (x) = G (x))$
36	32 35	imbi12d	$⊢ w = x \to ((X \in w \to F (w) = G (w)) \leftrightarrow (X \in x \to F (x) = G (x)))$
37	20	simp3d	$⊢ φ \to \forall w \in B (X \in w \to F (w) = G (w))$
38	37	ad3antrrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to \forall w \in B (X \in w \to F (w) = G (w))$
39	36 38 11	rspcdva	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to (X \in x \to F (x) = G (x))$
40	31 39	mpd	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to F (x) = G (x)$
41		simprl	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to F (x) \neq \emptyset$
42	40 41	eqnetrrd	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to G (x) \neq \emptyset$
43		fvn0elsupp	$⊢ ((B \in On \land x \in B) \land (G Fn B \land G (x) \neq \emptyset)) \to x \in {supp}_{\emptyset} (G)$
44	10 11 16 42 43	syl22anc	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to x \in {supp}_{\emptyset} (G)$

Metamath Proof Explorer

Theorem cantnflem1c

Proof