funpartlem

Description: Lemma for funpartfun . Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017)

		Ref	Expression
	Assertion	funpartlem	$⊢ A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \exists x F [\{A\}] = \{x\}$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \to A \in V$
2		vsnid	$⊢ x \in \{x\}$
3		eleq2	$⊢ F [\{A\}] = \{x\} \to (x \in F [\{A\}] \leftrightarrow x \in \{x\})$
4	2 3	mpbiri	$⊢ F [\{A\}] = \{x\} \to x \in F [\{A\}]$
5		n0i	$⊢ x \in F [\{A\}] \to \neg F [\{A\}] = \emptyset$
6		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
7	6	biimpi	$⊢ \neg A \in V \to \{A\} = \emptyset$
8	7	imaeq2d	$⊢ \neg A \in V \to F [\{A\}] = F [\emptyset]$
9		ima0	$⊢ F [\emptyset] = \emptyset$
10	8 9	eqtrdi	$⊢ \neg A \in V \to F [\{A\}] = \emptyset$
11	5 10	nsyl2	$⊢ x \in F [\{A\}] \to A \in V$
12	4 11	syl	$⊢ F [\{A\}] = \{x\} \to A \in V$
13	12	exlimiv	$⊢ \exists x F [\{A\}] = \{x\} \to A \in V$
14		eleq1	$⊢ y = A \to (y \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)))$
15		sneq	$⊢ y = A \to \{y\} = \{A\}$
16	15	imaeq2d	$⊢ y = A \to F [\{y\}] = F [\{A\}]$
17	16	eqeq1d	$⊢ y = A \to (F [\{y\}] = \{x\} \leftrightarrow F [\{A\}] = \{x\})$
18	17	exbidv	$⊢ y = A \to (\exists x F [\{y\}] = \{x\} \leftrightarrow \exists x F [\{A\}] = \{x\})$
19		vex	$⊢ y \in V$
20	19	eldm	$⊢ y \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \exists z y ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) z$
21		brxp	$⊢ y (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌) z \leftrightarrow (y \in V \land z \in 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
22	19 21	mpbiran	$⊢ y (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌) z \leftrightarrow z \in 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌$
23		elsingles	$⊢ z \in 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \leftrightarrow \exists x z = \{x\}$
24	22 23	bitri	$⊢ y (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌) z \leftrightarrow \exists x z = \{x\}$
25	24	anbi2i	$⊢ (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land y (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌) z) \leftrightarrow (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land \exists x z = \{x\})$
26		brin	$⊢ y ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) z \leftrightarrow (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land y (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌) z)$
27		19.42v	$⊢ \exists x (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z = \{x\}) \leftrightarrow (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land \exists x z = \{x\})$
28	25 26 27	3bitr4i	$⊢ y ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) z \leftrightarrow \exists x (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z = \{x\})$
29	28	exbii	$⊢ \exists z y ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) z \leftrightarrow \exists z \exists x (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z = \{x\})$
30		excom	$⊢ \exists z \exists x (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z = \{x\}) \leftrightarrow \exists x \exists z (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z = \{x\})$
31	29 30	bitri	$⊢ \exists z y ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) z \leftrightarrow \exists x \exists z (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z = \{x\})$
32		exancom	$⊢ \exists z (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z = \{x\}) \leftrightarrow \exists z (z = \{x\} \land y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z)$
33		snex	$⊢ \{x\} \in V$
34		breq2	$⊢ z = \{x\} \to (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \leftrightarrow y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \{x\})$
35	33 34	ceqsexv	$⊢ \exists z (z = \{x\} \land y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z) \leftrightarrow y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \{x\}$
36	19 33	brco	$⊢ y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \{x\} \leftrightarrow \exists z (y 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 z \land z 𝖨𝗆𝖺𝗀𝖾 F \{x\})$
37		vex	$⊢ z \in V$
38	19 37	brsingle	$⊢ y 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 z \leftrightarrow z = \{y\}$
39	38	anbi1i	$⊢ (y 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 z \land z 𝖨𝗆𝖺𝗀𝖾 F \{x\}) \leftrightarrow (z = \{y\} \land z 𝖨𝗆𝖺𝗀𝖾 F \{x\})$
40	39	exbii	$⊢ \exists z (y 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 z \land z 𝖨𝗆𝖺𝗀𝖾 F \{x\}) \leftrightarrow \exists z (z = \{y\} \land z 𝖨𝗆𝖺𝗀𝖾 F \{x\})$
41		snex	$⊢ \{y\} \in V$
42		breq1	$⊢ z = \{y\} \to (z 𝖨𝗆𝖺𝗀𝖾 F \{x\} \leftrightarrow \{y\} 𝖨𝗆𝖺𝗀𝖾 F \{x\})$
43	41 42	ceqsexv	$⊢ \exists z (z = \{y\} \land z 𝖨𝗆𝖺𝗀𝖾 F \{x\}) \leftrightarrow \{y\} 𝖨𝗆𝖺𝗀𝖾 F \{x\}$
44	41 33	brimage	$⊢ \{y\} 𝖨𝗆𝖺𝗀𝖾 F \{x\} \leftrightarrow \{x\} = F [\{y\}]$
45		eqcom	$⊢ \{x\} = F [\{y\}] \leftrightarrow F [\{y\}] = \{x\}$
46	43 44 45	3bitri	$⊢ \exists z (z = \{y\} \land z 𝖨𝗆𝖺𝗀𝖾 F \{x\}) \leftrightarrow F [\{y\}] = \{x\}$
47	36 40 46	3bitri	$⊢ y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \{x\} \leftrightarrow F [\{y\}] = \{x\}$
48	32 35 47	3bitri	$⊢ \exists z (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z = \{x\}) \leftrightarrow F [\{y\}] = \{x\}$
49	48	exbii	$⊢ \exists x \exists z (y (𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z = \{x\}) \leftrightarrow \exists x F [\{y\}] = \{x\}$
50	20 31 49	3bitri	$⊢ y \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \exists x F [\{y\}] = \{x\}$
51	14 18 50	vtoclbg	$⊢ A \in V \to (A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \exists x F [\{A\}] = \{x\})$
52	1 13 51	pm5.21nii	$⊢ A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \exists x F [\{A\}] = \{x\}$

Metamath Proof Explorer

Theorem funpartlem

Proof