dfac5lem4

	Ref	Expression
Hypotheses	dfac5lem.1	$⊢ A = \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\}$
	dfac5lem.2	$⊢ B = ⋃ A \cap y$
	dfac5lem.3	$⊢ φ \leftrightarrow \forall x ((\forall z \in x z \neq \emptyset \land \forall z \in x \forall w \in x (z \neq w \to z \cap w = \emptyset)) \to \exists y \forall z \in x \exists! v v \in (z \cap y))$
Assertion	dfac5lem4	$⊢ φ \to \exists y \forall z \in A \exists! v v \in (z \cap y)$

Proof

Step	Hyp	Ref	Expression
1		dfac5lem.1	$⊢ A = \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\}$
2		dfac5lem.2	$⊢ B = ⋃ A \cap y$
3		dfac5lem.3	$⊢ φ \leftrightarrow \forall x ((\forall z \in x z \neq \emptyset \land \forall z \in x \forall w \in x (z \neq w \to z \cap w = \emptyset)) \to \exists y \forall z \in x \exists! v v \in (z \cap y))$
4		vex	$⊢ z \in V$
5		neeq1	$⊢ u = z \to (u \neq \emptyset \leftrightarrow z \neq \emptyset)$
6		eqeq1	$⊢ u = z \to (u = \{t\} \times t \leftrightarrow z = \{t\} \times t)$
7	6	rexbidv	$⊢ u = z \to (\exists t \in h u = \{t\} \times t \leftrightarrow \exists t \in h z = \{t\} \times t)$
8	5 7	anbi12d	$⊢ u = z \to ((u \neq \emptyset \land \exists t \in h u = \{t\} \times t) \leftrightarrow (z \neq \emptyset \land \exists t \in h z = \{t\} \times t))$
9	4 8	elab	$⊢ z \in \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\} \leftrightarrow (z \neq \emptyset \land \exists t \in h z = \{t\} \times t)$
10	9	simplbi	$⊢ z \in \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\} \to z \neq \emptyset$
11	10 1	eleq2s	$⊢ z \in A \to z \neq \emptyset$
12	11	rgen	$⊢ \forall z \in A z \neq \emptyset$
13		df-an	$⊢ (x \in z \land x \in w) \leftrightarrow \neg (x \in z \to \neg x \in w)$
14	4 8 1	elab2	$⊢ z \in A \leftrightarrow (z \neq \emptyset \land \exists t \in h z = \{t\} \times t)$
15	14	simprbi	$⊢ z \in A \to \exists t \in h z = \{t\} \times t$
16		vex	$⊢ w \in V$
17		neeq1	$⊢ u = w \to (u \neq \emptyset \leftrightarrow w \neq \emptyset)$
18		eqeq1	$⊢ u = w \to (u = \{t\} \times t \leftrightarrow w = \{t\} \times t)$
19	18	rexbidv	$⊢ u = w \to (\exists t \in h u = \{t\} \times t \leftrightarrow \exists t \in h w = \{t\} \times t)$
20	17 19	anbi12d	$⊢ u = w \to ((u \neq \emptyset \land \exists t \in h u = \{t\} \times t) \leftrightarrow (w \neq \emptyset \land \exists t \in h w = \{t\} \times t))$
21	16 20 1	elab2	$⊢ w \in A \leftrightarrow (w \neq \emptyset \land \exists t \in h w = \{t\} \times t)$
22	21	simprbi	$⊢ w \in A \to \exists t \in h w = \{t\} \times t$
23		sneq	$⊢ t = g \to \{t\} = \{g\}$
24	23	xpeq1d	$⊢ t = g \to \{t\} \times t = \{g\} \times t$
25		xpeq2	$⊢ t = g \to \{g\} \times t = \{g\} \times g$
26	24 25	eqtrd	$⊢ t = g \to \{t\} \times t = \{g\} \times g$
27	26	eqeq2d	$⊢ t = g \to (w = \{t\} \times t \leftrightarrow w = \{g\} \times g)$
28	27	cbvrexvw	$⊢ \exists t \in h w = \{t\} \times t \leftrightarrow \exists g \in h w = \{g\} \times g$
29	22 28	sylib	$⊢ w \in A \to \exists g \in h w = \{g\} \times g$
30		eleq2	$⊢ z = \{t\} \times t \to (x \in z \leftrightarrow x \in (\{t\} \times t))$
31		elxp	$⊢ x \in (\{t\} \times t) \leftrightarrow \exists u \exists v (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t))$
32		excom	$⊢ \exists u \exists v (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \leftrightarrow \exists v \exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t))$
33	31 32	bitri	$⊢ x \in (\{t\} \times t) \leftrightarrow \exists v \exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t))$
34	30 33	bitrdi	$⊢ z = \{t\} \times t \to (x \in z \leftrightarrow \exists v \exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)))$
35		eleq2	$⊢ w = \{g\} \times g \to (x \in w \leftrightarrow x \in (\{g\} \times g))$
36		elxp	$⊢ x \in (\{g\} \times g) \leftrightarrow \exists u \exists y (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g))$
37		excom	$⊢ \exists u \exists y (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g)) \leftrightarrow \exists y \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g))$
38	36 37	bitri	$⊢ x \in (\{g\} \times g) \leftrightarrow \exists y \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g))$
39	35 38	bitrdi	$⊢ w = \{g\} \times g \to (x \in w \leftrightarrow \exists y \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g)))$
40	34 39	bi2anan9	$⊢ (z = \{t\} \times t \land w = \{g\} \times g) \to ((x \in z \land x \in w) \leftrightarrow (\exists v \exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \land \exists y \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g))))$
41		exdistrv	$⊢ \exists v \exists y (\exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \land \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g))) \leftrightarrow (\exists v \exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \land \exists y \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g)))$
42	40 41	bitr4di	$⊢ (z = \{t\} \times t \land w = \{g\} \times g) \to ((x \in z \land x \in w) \leftrightarrow \exists v \exists y (\exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \land \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g))))$
43		velsn	$⊢ u \in \{t\} \leftrightarrow u = t$
44		opeq1	$⊢ u = t \to ⟨u, v⟩ = ⟨t, v⟩$
45	44	eqeq2d	$⊢ u = t \to (x = ⟨u, v⟩ \leftrightarrow x = ⟨t, v⟩)$
46	45	biimpac	$⊢ (x = ⟨u, v⟩ \land u = t) \to x = ⟨t, v⟩$
47	43 46	sylan2b	$⊢ (x = ⟨u, v⟩ \land u \in \{t\}) \to x = ⟨t, v⟩$
48	47	adantrr	$⊢ (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \to x = ⟨t, v⟩$
49	48	exlimiv	$⊢ \exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \to x = ⟨t, v⟩$
50		velsn	$⊢ u \in \{g\} \leftrightarrow u = g$
51		opeq1	$⊢ u = g \to ⟨u, y⟩ = ⟨g, y⟩$
52	51	eqeq2d	$⊢ u = g \to (x = ⟨u, y⟩ \leftrightarrow x = ⟨g, y⟩)$
53	52	biimpac	$⊢ (x = ⟨u, y⟩ \land u = g) \to x = ⟨g, y⟩$
54	50 53	sylan2b	$⊢ (x = ⟨u, y⟩ \land u \in \{g\}) \to x = ⟨g, y⟩$
55	54	adantrr	$⊢ (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g)) \to x = ⟨g, y⟩$
56	55	exlimiv	$⊢ \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g)) \to x = ⟨g, y⟩$
57	49 56	sylan9req	$⊢ (\exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \land \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g))) \to ⟨t, v⟩ = ⟨g, y⟩$
58		vex	$⊢ t \in V$
59		vex	$⊢ v \in V$
60	58 59	opth1	$⊢ ⟨t, v⟩ = ⟨g, y⟩ \to t = g$
61	57 60	syl	$⊢ (\exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \land \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g))) \to t = g$
62	61	exlimivv	$⊢ \exists v \exists y (\exists u (x = ⟨u, v⟩ \land (u \in \{t\} \land v \in t)) \land \exists u (x = ⟨u, y⟩ \land (u \in \{g\} \land y \in g))) \to t = g$
63	42 62	syl6bi	$⊢ (z = \{t\} \times t \land w = \{g\} \times g) \to ((x \in z \land x \in w) \to t = g)$
64	63 26	syl6	$⊢ (z = \{t\} \times t \land w = \{g\} \times g) \to ((x \in z \land x \in w) \to \{t\} \times t = \{g\} \times g)$
65		eqeq12	$⊢ (z = \{t\} \times t \land w = \{g\} \times g) \to (z = w \leftrightarrow \{t\} \times t = \{g\} \times g)$
66	64 65	sylibrd	$⊢ (z = \{t\} \times t \land w = \{g\} \times g) \to ((x \in z \land x \in w) \to z = w)$
67	66	ex	$⊢ z = \{t\} \times t \to (w = \{g\} \times g \to ((x \in z \land x \in w) \to z = w))$
68	67	rexlimivw	$⊢ \exists t \in h z = \{t\} \times t \to (w = \{g\} \times g \to ((x \in z \land x \in w) \to z = w))$
69	68	rexlimdvw	$⊢ \exists t \in h z = \{t\} \times t \to (\exists g \in h w = \{g\} \times g \to ((x \in z \land x \in w) \to z = w))$
70	69	imp	$⊢ (\exists t \in h z = \{t\} \times t \land \exists g \in h w = \{g\} \times g) \to ((x \in z \land x \in w) \to z = w)$
71	15 29 70	syl2an	$⊢ (z \in A \land w \in A) \to ((x \in z \land x \in w) \to z = w)$
72	13 71	syl5bir	$⊢ (z \in A \land w \in A) \to (\neg (x \in z \to \neg x \in w) \to z = w)$
73	72	necon1ad	$⊢ (z \in A \land w \in A) \to (z \neq w \to (x \in z \to \neg x \in w))$
74	73	alrimdv	$⊢ (z \in A \land w \in A) \to (z \neq w \to \forall x (x \in z \to \neg x \in w))$
75		disj1	$⊢ z \cap w = \emptyset \leftrightarrow \forall x (x \in z \to \neg x \in w)$
76	74 75	syl6ibr	$⊢ (z \in A \land w \in A) \to (z \neq w \to z \cap w = \emptyset)$
77	76	rgen2	$⊢ \forall z \in A \forall w \in A (z \neq w \to z \cap w = \emptyset)$
78		vex	$⊢ h \in V$
79		vuniex	$⊢ ⋃ h \in V$
80	78 79	xpex	$⊢ h \times ⋃ h \in V$
81	80	pwex	$⊢ 𝒫 (h \times ⋃ h) \in V$
82		snssi	$⊢ t \in h \to \{t\} \subseteq h$
83		elssuni	$⊢ t \in h \to t \subseteq ⋃ h$
84		xpss12	$⊢ (\{t\} \subseteq h \land t \subseteq ⋃ h) \to \{t\} \times t \subseteq h \times ⋃ h$
85	82 83 84	syl2anc	$⊢ t \in h \to \{t\} \times t \subseteq h \times ⋃ h$
86		snex	$⊢ \{t\} \in V$
87	86 58	xpex	$⊢ \{t\} \times t \in V$
88	87	elpw	$⊢ \{t\} \times t \in 𝒫 (h \times ⋃ h) \leftrightarrow \{t\} \times t \subseteq h \times ⋃ h$
89	85 88	sylibr	$⊢ t \in h \to \{t\} \times t \in 𝒫 (h \times ⋃ h)$
90		eleq1	$⊢ u = \{t\} \times t \to (u \in 𝒫 (h \times ⋃ h) \leftrightarrow \{t\} \times t \in 𝒫 (h \times ⋃ h))$
91	89 90	syl5ibrcom	$⊢ t \in h \to (u = \{t\} \times t \to u \in 𝒫 (h \times ⋃ h))$
92	91	rexlimiv	$⊢ \exists t \in h u = \{t\} \times t \to u \in 𝒫 (h \times ⋃ h)$
93	92	adantl	$⊢ (u \neq \emptyset \land \exists t \in h u = \{t\} \times t) \to u \in 𝒫 (h \times ⋃ h)$
94	93	abssi	$⊢ \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\} \subseteq 𝒫 (h \times ⋃ h)$
95	81 94	ssexi	$⊢ \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\} \in V$
96	1 95	eqeltri	$⊢ A \in V$
97		raleq	$⊢ x = A \to (\forall z \in x z \neq \emptyset \leftrightarrow \forall z \in A z \neq \emptyset)$
98		raleq	$⊢ x = A \to (\forall w \in x (z \neq w \to z \cap w = \emptyset) \leftrightarrow \forall w \in A (z \neq w \to z \cap w = \emptyset))$
99	98	raleqbi1dv	$⊢ x = A \to (\forall z \in x \forall w \in x (z \neq w \to z \cap w = \emptyset) \leftrightarrow \forall z \in A \forall w \in A (z \neq w \to z \cap w = \emptyset))$
100	97 99	anbi12d	$⊢ x = A \to ((\forall z \in x z \neq \emptyset \land \forall z \in x \forall w \in x (z \neq w \to z \cap w = \emptyset)) \leftrightarrow (\forall z \in A z \neq \emptyset \land \forall z \in A \forall w \in A (z \neq w \to z \cap w = \emptyset)))$
101		raleq	$⊢ x = A \to (\forall z \in x \exists! v v \in (z \cap y) \leftrightarrow \forall z \in A \exists! v v \in (z \cap y))$
102	101	exbidv	$⊢ x = A \to (\exists y \forall z \in x \exists! v v \in (z \cap y) \leftrightarrow \exists y \forall z \in A \exists! v v \in (z \cap y))$
103	100 102	imbi12d	$⊢ x = A \to (((\forall z \in x z \neq \emptyset \land \forall z \in x \forall w \in x (z \neq w \to z \cap w = \emptyset)) \to \exists y \forall z \in x \exists! v v \in (z \cap y)) \leftrightarrow ((\forall z \in A z \neq \emptyset \land \forall z \in A \forall w \in A (z \neq w \to z \cap w = \emptyset)) \to \exists y \forall z \in A \exists! v v \in (z \cap y)))$
104	96 103	spcv	$⊢ \forall x ((\forall z \in x z \neq \emptyset \land \forall z \in x \forall w \in x (z \neq w \to z \cap w = \emptyset)) \to \exists y \forall z \in x \exists! v v \in (z \cap y)) \to ((\forall z \in A z \neq \emptyset \land \forall z \in A \forall w \in A (z \neq w \to z \cap w = \emptyset)) \to \exists y \forall z \in A \exists! v v \in (z \cap y))$
105	3 104	sylbi	$⊢ φ \to ((\forall z \in A z \neq \emptyset \land \forall z \in A \forall w \in A (z \neq w \to z \cap w = \emptyset)) \to \exists y \forall z \in A \exists! v v \in (z \cap y))$
106	12 77 105	mp2ani	$⊢ φ \to \exists y \forall z \in A \exists! v v \in (z \cap y)$

Metamath Proof Explorer

Theorem dfac5lem4

Proof