dfttc4lem2

		Ref	Expression
	Hypothesis	dfttc4lem2.1	$⊢ B = \{x \| \exists y (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = x))\}$
	Assertion	dfttc4lem2	$⊢ (A \subseteq B \land Tr B)$

Proof

Step	Hyp	Ref	Expression
1		dfttc4lem2.1	$⊢ B = \{x \| \exists y (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = x))\}$
2		disjsn	$⊢ A \cap \{u\} = \emptyset \leftrightarrow \neg u \in A$
3	2	biimpi	$⊢ A \cap \{u\} = \emptyset \to \neg u \in A$
4	3	necon2ai	$⊢ u \in A \to A \cap \{u\} \neq \emptyset$
5		elsni	$⊢ z \in \{u\} \to z = u$
6	5	a1d	$⊢ z \in \{u\} \to (z \cap \{u\} = \emptyset \to z = u)$
7	6	rgen	$⊢ \forall z \in \{u\} (z \cap \{u\} = \emptyset \to z = u)$
8		vsnex	$⊢ \{u\} \in V$
9		vex	$⊢ u \in V$
10	1 8 9	dfttc4lem1	$⊢ (A \cap \{u\} \neq \emptyset \land \forall z \in \{u\} (z \cap \{u\} = \emptyset \to z = u)) \to u \in B$
11	4 7 10	sylancl	$⊢ u \in A \to u \in B$
12	11	ssriv	$⊢ A \subseteq B$
13		vex	$⊢ v \in V$
14		simpr	$⊢ (x = v \land y = w) \to y = w$
15	14	ineq2d	$⊢ (x = v \land y = w) \to A \cap y = A \cap w$
16	15	neeq1d	$⊢ (x = v \land y = w) \to (A \cap y \neq \emptyset \leftrightarrow A \cap w \neq \emptyset)$
17	14	ineq2d	$⊢ (x = v \land y = w) \to z \cap y = z \cap w$
18	17	eqeq1d	$⊢ (x = v \land y = w) \to (z \cap y = \emptyset \leftrightarrow z \cap w = \emptyset)$
19		simpl	$⊢ (x = v \land y = w) \to x = v$
20	19	eqeq2d	$⊢ (x = v \land y = w) \to (z = x \leftrightarrow z = v)$
21	18 20	imbi12d	$⊢ (x = v \land y = w) \to ((z \cap y = \emptyset \to z = x) \leftrightarrow (z \cap w = \emptyset \to z = v))$
22	14 21	raleqbidvv	$⊢ (x = v \land y = w) \to (\forall z \in y (z \cap y = \emptyset \to z = x) \leftrightarrow \forall z \in w (z \cap w = \emptyset \to z = v))$
23	16 22	anbi12d	$⊢ (x = v \land y = w) \to ((A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = x)) \leftrightarrow (A \cap w \neq \emptyset \land \forall z \in w (z \cap w = \emptyset \to z = v)))$
24	23	cbvexdvaw	$⊢ x = v \to (\exists y (A \cap y \neq \emptyset \land \forall z \in y (z \cap y = \emptyset \to z = x)) \leftrightarrow \exists w (A \cap w \neq \emptyset \land \forall z \in w (z \cap w = \emptyset \to z = v)))$
25	13 24 1	elab2	$⊢ v \in B \leftrightarrow \exists w (A \cap w \neq \emptyset \land \forall z \in w (z \cap w = \emptyset \to z = v))$
26		undisj2	$⊢ (A \cap w = \emptyset \land A \cap \{u\} = \emptyset) \leftrightarrow A \cap (w \cup \{u\}) = \emptyset$
27	26	biimpri	$⊢ A \cap (w \cup \{u\}) = \emptyset \to (A \cap w = \emptyset \land A \cap \{u\} = \emptyset)$
28	27	simpld	$⊢ A \cap (w \cup \{u\}) = \emptyset \to A \cap w = \emptyset$
29	28	necon3i	$⊢ A \cap w \neq \emptyset \to A \cap (w \cup \{u\}) \neq \emptyset$
30	29	a1i	$⊢ u \in v \to (A \cap w \neq \emptyset \to A \cap (w \cup \{u\}) \neq \emptyset)$
31		undisj2	$⊢ (z \cap w = \emptyset \land z \cap \{u\} = \emptyset) \leftrightarrow z \cap (w \cup \{u\}) = \emptyset$
32	31	biimpri	$⊢ z \cap (w \cup \{u\}) = \emptyset \to (z \cap w = \emptyset \land z \cap \{u\} = \emptyset)$
33	32	simpld	$⊢ z \cap (w \cup \{u\}) = \emptyset \to z \cap w = \emptyset$
34	33	imim1i	$⊢ (z \cap w = \emptyset \to z = v) \to (z \cap (w \cup \{u\}) = \emptyset \to z = v)$
35	32	simprd	$⊢ z \cap (w \cup \{u\}) = \emptyset \to z \cap \{u\} = \emptyset$
36		disjsn	$⊢ z \cap \{u\} = \emptyset \leftrightarrow \neg u \in z$
37	35 36	sylib	$⊢ z \cap (w \cup \{u\}) = \emptyset \to \neg u \in z$
38		elequ2	$⊢ z = v \to (u \in z \leftrightarrow u \in v)$
39	38	biimprd	$⊢ z = v \to (u \in v \to u \in z)$
40	39	con3d	$⊢ z = v \to (\neg u \in z \to \neg u \in v)$
41		pm2.21	$⊢ \neg u \in v \to (u \in v \to z = u)$
42	37 40 41	syl56	$⊢ z = v \to (z \cap (w \cup \{u\}) = \emptyset \to (u \in v \to z = u))$
43	34 42	syli	$⊢ (z \cap w = \emptyset \to z = v) \to (z \cap (w \cup \{u\}) = \emptyset \to (u \in v \to z = u))$
44	43	com3r	$⊢ u \in v \to ((z \cap w = \emptyset \to z = v) \to (z \cap (w \cup \{u\}) = \emptyset \to z = u))$
45	44	ralimdv	$⊢ u \in v \to (\forall z \in w (z \cap w = \emptyset \to z = v) \to \forall z \in w (z \cap (w \cup \{u\}) = \emptyset \to z = u))$
46	5	a1d	$⊢ z \in \{u\} \to (z \cap (w \cup \{u\}) = \emptyset \to z = u)$
47	46	rgen	$⊢ \forall z \in \{u\} (z \cap (w \cup \{u\}) = \emptyset \to z = u)$
48		ralun	$⊢ (\forall z \in w (z \cap (w \cup \{u\}) = \emptyset \to z = u) \land \forall z \in \{u\} (z \cap (w \cup \{u\}) = \emptyset \to z = u)) \to \forall z \in (w \cup \{u\}) (z \cap (w \cup \{u\}) = \emptyset \to z = u)$
49	47 48	mpan2	$⊢ \forall z \in w (z \cap (w \cup \{u\}) = \emptyset \to z = u) \to \forall z \in (w \cup \{u\}) (z \cap (w \cup \{u\}) = \emptyset \to z = u)$
50	45 49	syl6	$⊢ u \in v \to (\forall z \in w (z \cap w = \emptyset \to z = v) \to \forall z \in (w \cup \{u\}) (z \cap (w \cup \{u\}) = \emptyset \to z = u))$
51	30 50	anim12d	$⊢ u \in v \to ((A \cap w \neq \emptyset \land \forall z \in w (z \cap w = \emptyset \to z = v)) \to (A \cap (w \cup \{u\}) \neq \emptyset \land \forall z \in (w \cup \{u\}) (z \cap (w \cup \{u\}) = \emptyset \to z = u)))$
52		vex	$⊢ w \in V$
53	52 8	unex	$⊢ w \cup \{u\} \in V$
54	1 53 9	dfttc4lem1	$⊢ (A \cap (w \cup \{u\}) \neq \emptyset \land \forall z \in (w \cup \{u\}) (z \cap (w \cup \{u\}) = \emptyset \to z = u)) \to u \in B$
55	51 54	syl6	$⊢ u \in v \to ((A \cap w \neq \emptyset \land \forall z \in w (z \cap w = \emptyset \to z = v)) \to u \in B)$
56	55	exlimdv	$⊢ u \in v \to (\exists w (A \cap w \neq \emptyset \land \forall z \in w (z \cap w = \emptyset \to z = v)) \to u \in B)$
57	25 56	biimtrid	$⊢ u \in v \to (v \in B \to u \in B)$
58	57	imp	$⊢ (u \in v \land v \in B) \to u \in B$
59	58	gen2	$⊢ \forall u \forall v ((u \in v \land v \in B) \to u \in B)$
60		dftr2	$⊢ Tr B \leftrightarrow \forall u \forall v ((u \in v \land v \in B) \to u \in B)$
61	59 60	mpbir	$⊢ Tr B$
62	12 61	pm3.2i	$⊢ (A \subseteq B \land Tr B)$

Metamath Proof Explorer

Theorem dfttc4lem2

Proof