mptsnunlem

Description: This is the core of the proof of mptsnun , but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020)

	Ref	Expression
Hypotheses	mptsnun.f	$⊢ F = (x \in A ⟼ \{x\})$
	mptsnun.r	$⊢ R = \{u \| \exists x \in A u = \{x\}\}$
Assertion	mptsnunlem	$⊢ B \subseteq A \to B = ⋃ F [B]$

Proof

Step	Hyp	Ref	Expression
1		mptsnun.f	$⊢ F = (x \in A ⟼ \{x\})$
2		mptsnun.r	$⊢ R = \{u \| \exists x \in A u = \{x\}\}$
3		df-ima	$⊢ F [B] = ran ({F ↾}_{B})$
4	1	reseq1i	$⊢ {F ↾}_{B} = {(x \in A ⟼ \{x\}) ↾}_{B}$
5		resmpt	$⊢ B \subseteq A \to {(x \in A ⟼ \{x\}) ↾}_{B} = (x \in B ⟼ \{x\})$
6	4 5	eqtrid	$⊢ B \subseteq A \to {F ↾}_{B} = (x \in B ⟼ \{x\})$
7	6	rneqd	$⊢ B \subseteq A \to ran ({F ↾}_{B}) = ran (x \in B ⟼ \{x\})$
8		rnmptsn	$⊢ ran (x \in B ⟼ \{x\}) = \{u \| \exists x \in B u = \{x\}\}$
9	7 8	eqtrdi	$⊢ B \subseteq A \to ran ({F ↾}_{B}) = \{u \| \exists x \in B u = \{x\}\}$
10	3 9	eqtrid	$⊢ B \subseteq A \to F [B] = \{u \| \exists x \in B u = \{x\}\}$
11	10	unieqd	$⊢ B \subseteq A \to ⋃ F [B] = ⋃ \{u \| \exists x \in B u = \{x\}\}$
12	11	eleq2d	$⊢ B \subseteq A \to (x \in ⋃ F [B] \leftrightarrow x \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
13		eleq1w	$⊢ z = x \to (z \in B \leftrightarrow x \in B)$
14		eluniab	$⊢ z \in ⋃ \{u \| \exists x \in B u = \{x\}\} \leftrightarrow \exists u (z \in u \land \exists x \in B u = \{x\})$
15		ancom	$⊢ (z \in u \land \exists x \in B u = \{x\}) \leftrightarrow (\exists x \in B u = \{x\} \land z \in u)$
16		r19.41v	$⊢ \exists x \in B (u = \{x\} \land z \in u) \leftrightarrow (\exists x \in B u = \{x\} \land z \in u)$
17		df-rex	$⊢ \exists x \in B (u = \{x\} \land z \in u) \leftrightarrow \exists x (x \in B \land (u = \{x\} \land z \in u))$
18	15 16 17	3bitr2i	$⊢ (z \in u \land \exists x \in B u = \{x\}) \leftrightarrow \exists x (x \in B \land (u = \{x\} \land z \in u))$
19		eleq2	$⊢ u = \{x\} \to (z \in u \leftrightarrow z \in \{x\})$
20	19	anbi2d	$⊢ u = \{x\} \to ((u = \{x\} \land z \in u) \leftrightarrow (u = \{x\} \land z \in \{x\}))$
21	20	adantr	$⊢ (u = \{x\} \land z \in u) \to ((u = \{x\} \land z \in u) \leftrightarrow (u = \{x\} \land z \in \{x\}))$
22	21	ibi	$⊢ (u = \{x\} \land z \in u) \to (u = \{x\} \land z \in \{x\})$
23	22	anim2i	$⊢ (x \in B \land (u = \{x\} \land z \in u)) \to (x \in B \land (u = \{x\} \land z \in \{x\}))$
24	23	eximi	$⊢ \exists x (x \in B \land (u = \{x\} \land z \in u)) \to \exists x (x \in B \land (u = \{x\} \land z \in \{x\}))$
25	18 24	sylbi	$⊢ (z \in u \land \exists x \in B u = \{x\}) \to \exists x (x \in B \land (u = \{x\} \land z \in \{x\}))$
26		an12	$⊢ (x \in B \land (u = \{x\} \land z \in \{x\})) \leftrightarrow (u = \{x\} \land (x \in B \land z \in \{x\}))$
27	26	exbii	$⊢ \exists x (x \in B \land (u = \{x\} \land z \in \{x\})) \leftrightarrow \exists x (u = \{x\} \land (x \in B \land z \in \{x\}))$
28		exsimpr	$⊢ \exists x (u = \{x\} \land (x \in B \land z \in \{x\})) \to \exists x (x \in B \land z \in \{x\})$
29	27 28	sylbi	$⊢ \exists x (x \in B \land (u = \{x\} \land z \in \{x\})) \to \exists x (x \in B \land z \in \{x\})$
30	25 29	syl	$⊢ (z \in u \land \exists x \in B u = \{x\}) \to \exists x (x \in B \land z \in \{x\})$
31	30	exlimiv	$⊢ \exists u (z \in u \land \exists x \in B u = \{x\}) \to \exists x (x \in B \land z \in \{x\})$
32	14 31	sylbi	$⊢ z \in ⋃ \{u \| \exists x \in B u = \{x\}\} \to \exists x (x \in B \land z \in \{x\})$
33		velsn	$⊢ z \in \{x\} \leftrightarrow z = x$
34	33	anbi2i	$⊢ (x \in B \land z \in \{x\}) \leftrightarrow (x \in B \land z = x)$
35	34	exbii	$⊢ \exists x (x \in B \land z \in \{x\}) \leftrightarrow \exists x (x \in B \land z = x)$
36	32 35	sylib	$⊢ z \in ⋃ \{u \| \exists x \in B u = \{x\}\} \to \exists x (x \in B \land z = x)$
37	13	biimparc	$⊢ (x \in B \land z = x) \to z \in B$
38	37	exlimiv	$⊢ \exists x (x \in B \land z = x) \to z \in B$
39	36 38	syl	$⊢ z \in ⋃ \{u \| \exists x \in B u = \{x\}\} \to z \in B$
40	13 39	vtoclga	$⊢ x \in ⋃ \{u \| \exists x \in B u = \{x\}\} \to x \in B$
41		equid	$⊢ x = x$
42		eqid	$⊢ \{x\} = \{x\}$
43		vsnex	$⊢ \{x\} \in V$
44		sbcg	$⊢ \{x\} \in V \to (\underset{˙}{[} \{x\} / u \underset{˙}{]} x \in B \leftrightarrow x \in B)$
45	43 44	ax-mp	$⊢ \underset{˙}{[} \{x\} / u \underset{˙}{]} x \in B \leftrightarrow x \in B$
46		eqsbc1	$⊢ \{x\} \in V \to (\underset{˙}{[} \{x\} / u \underset{˙}{]} u = \{x\} \leftrightarrow \{x\} = \{x\})$
47	43 46	ax-mp	$⊢ \underset{˙}{[} \{x\} / u \underset{˙}{]} u = \{x\} \leftrightarrow \{x\} = \{x\}$
48	19	adantl	$⊢ (x \in B \land u = \{x\}) \to (z \in u \leftrightarrow z \in \{x\})$
49		df-rex	$⊢ \exists x \in B u = \{x\} \leftrightarrow \exists x (x \in B \land u = \{x\})$
50	14	biimpri	$⊢ \exists u (z \in u \land \exists x \in B u = \{x\}) \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\}$
51	50	19.23bi	$⊢ (z \in u \land \exists x \in B u = \{x\}) \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\}$
52	51	expcom	$⊢ \exists x \in B u = \{x\} \to (z \in u \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
53	49 52	sylbir	$⊢ \exists x (x \in B \land u = \{x\}) \to (z \in u \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
54	53	19.23bi	$⊢ (x \in B \land u = \{x\}) \to (z \in u \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
55	48 54	sylbird	$⊢ (x \in B \land u = \{x\}) \to (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
56	55	sbcth	$⊢ \{x\} \in V \to \underset{˙}{[} \{x\} / u \underset{˙}{]} ((x \in B \land u = \{x\}) \to (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\}))$
57	43 56	ax-mp	$⊢ \underset{˙}{[} \{x\} / u \underset{˙}{]} ((x \in B \land u = \{x\}) \to (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\}))$
58		sbcimg	$⊢ \{x\} \in V \to (\underset{˙}{[} \{x\} / u \underset{˙}{]} ((x \in B \land u = \{x\}) \to (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})) \leftrightarrow (\underset{˙}{[} \{x\} / u \underset{˙}{]} (x \in B \land u = \{x\}) \to \underset{˙}{[} \{x\} / u \underset{˙}{]} (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})))$
59	43 58	ax-mp	$⊢ \underset{˙}{[} \{x\} / u \underset{˙}{]} ((x \in B \land u = \{x\}) \to (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})) \leftrightarrow (\underset{˙}{[} \{x\} / u \underset{˙}{]} (x \in B \land u = \{x\}) \to \underset{˙}{[} \{x\} / u \underset{˙}{]} (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\}))$
60	57 59	mpbi	$⊢ \underset{˙}{[} \{x\} / u \underset{˙}{]} (x \in B \land u = \{x\}) \to \underset{˙}{[} \{x\} / u \underset{˙}{]} (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
61		sbcan	$⊢ \underset{˙}{[} \{x\} / u \underset{˙}{]} (x \in B \land u = \{x\}) \leftrightarrow (\underset{˙}{[} \{x\} / u \underset{˙}{]} x \in B \land \underset{˙}{[} \{x\} / u \underset{˙}{]} u = \{x\})$
62		nfv	$⊢ Ⅎ u z \in \{x\}$
63		nfab1	$⊢ \underline{Ⅎ} u \{u \| \exists x \in B u = \{x\}\}$
64	63	nfuni	$⊢ \underline{Ⅎ} u ⋃ \{u \| \exists x \in B u = \{x\}\}$
65	64	nfcri	$⊢ Ⅎ u z \in ⋃ \{u \| \exists x \in B u = \{x\}\}$
66	62 65	nfim	$⊢ Ⅎ u (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
67	43 66	sbcgfi	$⊢ \underset{˙}{[} \{x\} / u \underset{˙}{]} (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\}) \leftrightarrow (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
68	60 61 67	3imtr3i	$⊢ (\underset{˙}{[} \{x\} / u \underset{˙}{]} x \in B \land \underset{˙}{[} \{x\} / u \underset{˙}{]} u = \{x\}) \to (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
69	45 47 68	syl2anbr	$⊢ (x \in B \land \{x\} = \{x\}) \to (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
70	42 69	mpan2	$⊢ x \in B \to (z \in \{x\} \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
71	33 70	biimtrrid	$⊢ x \in B \to (z = x \to z \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
72		eleq1w	$⊢ z = x \to (z \in ⋃ \{u \| \exists x \in B u = \{x\}\} \leftrightarrow x \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
73	71 72	mpbidi	$⊢ x \in B \to (z = x \to x \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
74	73	com12	$⊢ z = x \to (x \in B \to x \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
75	74	sbimi	$⊢ [x/ z] z = x \to [x/ z] (x \in B \to x \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
76		equsb3	$⊢ [x/ z] z = x \leftrightarrow x = x$
77		sbv	$⊢ [x/ z] (x \in B \to x \in ⋃ \{u \| \exists x \in B u = \{x\}\}) \leftrightarrow (x \in B \to x \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
78	75 76 77	3imtr3i	$⊢ x = x \to (x \in B \to x \in ⋃ \{u \| \exists x \in B u = \{x\}\})$
79	41 78	ax-mp	$⊢ x \in B \to x \in ⋃ \{u \| \exists x \in B u = \{x\}\}$
80	40 79	impbii	$⊢ x \in ⋃ \{u \| \exists x \in B u = \{x\}\} \leftrightarrow x \in B$
81	12 80	bitrdi	$⊢ B \subseteq A \to (x \in ⋃ F [B] \leftrightarrow x \in B)$
82	81	eqrdv	$⊢ B \subseteq A \to ⋃ F [B] = B$
83	82	eqcomd	$⊢ B \subseteq A \to B = ⋃ F [B]$

Metamath Proof Explorer

Theorem mptsnunlem

Proof