cantnflem1a

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

	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)\}$
Assertion	cantnflem1a	$⊢ φ \to X \in {supp}_{\emptyset} (G)$

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	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)))$
10	9	simp1d	$⊢ φ \to X \in B$
11	9	simp2d	$⊢ φ \to F (X) \in G (X)$
12	11	ne0d	$⊢ φ \to G (X) \neq \emptyset$
13	1 2 3	cantnfs	$⊢ φ \to (G \in S \leftrightarrow (G : B ⟶ A \land {finSupp}_{\emptyset} (G)))$
14	6 13	mpbid	$⊢ φ \to (G : B ⟶ A \land {finSupp}_{\emptyset} (G))$
15	14	simpld	$⊢ φ \to G : B ⟶ A$
16	15	ffnd	$⊢ φ \to G Fn B$
17		0ex	$⊢ \emptyset \in V$
18	17	a1i	$⊢ φ \to \emptyset \in V$
19		elsuppfn	$⊢ (G Fn B \land B \in On \land \emptyset \in V) \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \neq \emptyset))$
20	16 3 18 19	syl3anc	$⊢ φ \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \neq \emptyset))$
21	10 12 20	mpbir2and	$⊢ φ \to X \in {supp}_{\emptyset} (G)$

Metamath Proof Explorer