cantnfp1lem1

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 20-Jun-2015) (Revised by AV, 30-Jun-2019)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	cantnfp1.g	$⊢ φ \to G \in S$
	cantnfp1.x	$⊢ φ \to X \in B$
	cantnfp1.y	$⊢ φ \to Y \in A$
	cantnfp1.s	$⊢ φ \to G supp \emptyset \subseteq X$
	cantnfp1.f	$⊢ F = (t \in B ⟼ if (t = X, Y, G (t)))$
Assertion	cantnfp1lem1	$⊢ φ \to F \in S$

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		cantnfp1.g	$⊢ φ \to G \in S$
5		cantnfp1.x	$⊢ φ \to X \in B$
6		cantnfp1.y	$⊢ φ \to Y \in A$
7		cantnfp1.s	$⊢ φ \to G supp \emptyset \subseteq X$
8		cantnfp1.f	$⊢ F = (t \in B ⟼ if (t = X, Y, G (t)))$
9	6	adantr	$⊢ (φ \land t \in B) \to Y \in A$
10	1 2 3	cantnfs	$⊢ φ \to (G \in S \leftrightarrow (G : B ⟶ A \land {finSupp}_{\emptyset} (G)))$
11	4 10	mpbid	$⊢ φ \to (G : B ⟶ A \land {finSupp}_{\emptyset} (G))$
12	11	simpld	$⊢ φ \to G : B ⟶ A$
13	12	ffvelcdmda	$⊢ (φ \land t \in B) \to G (t) \in A$
14	9 13	ifcld	$⊢ (φ \land t \in B) \to if (t = X, Y, G (t)) \in A$
15	14 8	fmptd	$⊢ φ \to F : B ⟶ A$
16	11	simprd	$⊢ φ \to {finSupp}_{\emptyset} (G)$
17	16	fsuppimpd	$⊢ φ \to G supp \emptyset \in Fin$
18		snfi	$⊢ \{X\} \in Fin$
19		unfi	$⊢ (G supp \emptyset \in Fin \land \{X\} \in Fin) \to {supp}_{\emptyset} (G) \cup \{X\} \in Fin$
20	17 18 19	sylancl	$⊢ φ \to {supp}_{\emptyset} (G) \cup \{X\} \in Fin$
21		eqeq1	$⊢ t = k \to (t = X \leftrightarrow k = X)$
22		fveq2	$⊢ t = k \to G (t) = G (k)$
23	21 22	ifbieq2d	$⊢ t = k \to if (t = X, Y, G (t)) = if (k = X, Y, G (k))$
24		eldifi	$⊢ k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\})) \to k \in B$
25	24	adantl	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to k \in B$
26	6	adantr	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to Y \in A$
27		fvex	$⊢ G (k) \in V$
28		ifexg	$⊢ (Y \in A \land G (k) \in V) \to if (k = X, Y, G (k)) \in V$
29	26 27 28	sylancl	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to if (k = X, Y, G (k)) \in V$
30	8 23 25 29	fvmptd3	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to F (k) = if (k = X, Y, G (k))$
31		eldifn	$⊢ k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\})) \to \neg k \in ({supp}_{\emptyset} (G) \cup \{X\})$
32	31	adantl	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to \neg k \in ({supp}_{\emptyset} (G) \cup \{X\})$
33		velsn	$⊢ k \in \{X\} \leftrightarrow k = X$
34		elun2	$⊢ k \in \{X\} \to k \in ({supp}_{\emptyset} (G) \cup \{X\})$
35	33 34	sylbir	$⊢ k = X \to k \in ({supp}_{\emptyset} (G) \cup \{X\})$
36	32 35	nsyl	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to \neg k = X$
37	36	iffalsed	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to if (k = X, Y, G (k)) = G (k)$
38		ssun1	$⊢ G supp \emptyset \subseteq {supp}_{\emptyset} (G) \cup \{X\}$
39		sscon	$⊢ G supp \emptyset \subseteq {supp}_{\emptyset} (G) \cup \{X\} \to B ∖ ({supp}_{\emptyset} (G) \cup \{X\}) \subseteq B ∖ {supp}_{\emptyset} (G)$
40	38 39	ax-mp	$⊢ B ∖ ({supp}_{\emptyset} (G) \cup \{X\}) \subseteq B ∖ {supp}_{\emptyset} (G)$
41	40	sseli	$⊢ k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\})) \to k \in (B ∖ {supp}_{\emptyset} (G))$
42		ssidd	$⊢ φ \to G supp \emptyset \subseteq G supp \emptyset$
43		0ex	$⊢ \emptyset \in V$
44	43	a1i	$⊢ φ \to \emptyset \in V$
45	12 42 3 44	suppssr	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (G))) \to G (k) = \emptyset$
46	41 45	sylan2	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to G (k) = \emptyset$
47	30 37 46	3eqtrd	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to F (k) = \emptyset$
48	15 47	suppss	$⊢ φ \to F supp \emptyset \subseteq {supp}_{\emptyset} (G) \cup \{X\}$
49	20 48	ssfid	$⊢ φ \to F supp \emptyset \in Fin$
50	8	funmpt2	$⊢ Fun F$
51		mptexg	$⊢ B \in On \to (t \in B ⟼ if (t = X, Y, G (t))) \in V$
52	8 51	eqeltrid	$⊢ B \in On \to F \in V$
53	3 52	syl	$⊢ φ \to F \in V$
54		funisfsupp	$⊢ (Fun F \land F \in V \land \emptyset \in V) \to ({finSupp}_{\emptyset} (F) \leftrightarrow F supp \emptyset \in Fin)$
55	50 53 44 54	mp3an2i	$⊢ φ \to ({finSupp}_{\emptyset} (F) \leftrightarrow F supp \emptyset \in Fin)$
56	49 55	mpbird	$⊢ φ \to {finSupp}_{\emptyset} (F)$
57	1 2 3	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : B ⟶ A \land {finSupp}_{\emptyset} (F)))$
58	15 56 57	mpbir2and	$⊢ φ \to F \in S$

Metamath Proof Explorer

Theorem cantnfp1lem1

Proof