dfac5lem4

Description: Lemma for dfac5 . (Contributed by NM, 11-Apr-2004) Avoid ax-11 . (Revised by BTernaryTau, 23-Jun-2025)

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

Metamath Proof Explorer

Theorem dfac5lem4

Proof