oprabidw

Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Version of oprabid with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 20-Mar-2013) Avoid ax-13 . (Revised by Gino Giotto, 26-Jan-2024)

		Ref	Expression
	Assertion	oprabidw	$⊢ ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow φ$

Proof

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨⟨x, y⟩, z⟩ \in V$
2		opex	$⊢ ⟨x, y⟩ \in V$
3		vex	$⊢ z \in V$
4	2 3	eqvinop	$⊢ w = ⟨⟨x, y⟩, z⟩ \leftrightarrow \exists a \exists t (w = ⟨a, t⟩ \land ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩)$
5	4	biimpi	$⊢ w = ⟨⟨x, y⟩, z⟩ \to \exists a \exists t (w = ⟨a, t⟩ \land ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩)$
6		eqeq1	$⊢ w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩)$
7		vex	$⊢ a \in V$
8		vex	$⊢ t \in V$
9	7 8	opth1	$⊢ ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩ \to a = ⟨x, y⟩$
10	6 9	syl6bi	$⊢ w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to a = ⟨x, y⟩)$
11		vex	$⊢ x \in V$
12		vex	$⊢ y \in V$
13	11 12	eqvinop	$⊢ a = ⟨x, y⟩ \leftrightarrow \exists r \exists s (a = ⟨r, s⟩ \land ⟨r, s⟩ = ⟨x, y⟩)$
14		opeq1	$⊢ a = ⟨r, s⟩ \to ⟨a, t⟩ = ⟨⟨r, s⟩, t⟩$
15	14	eqeq2d	$⊢ a = ⟨r, s⟩ \to (w = ⟨a, t⟩ \leftrightarrow w = ⟨⟨r, s⟩, t⟩)$
16	11 12 3	otth2	$⊢ ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \leftrightarrow (x = r \land y = s \land z = t)$
17		euequ	$⊢ \exists! x x = r$
18		eupick	$⊢ (\exists! x x = r \land \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))) \to (x = r \to \exists y (y = s \land \exists z (z = t \land φ)))$
19	17 18	mpan	$⊢ \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ))) \to (x = r \to \exists y (y = s \land \exists z (z = t \land φ)))$
20		euequ	$⊢ \exists! y y = s$
21		eupick	$⊢ (\exists! y y = s \land \exists y (y = s \land \exists z (z = t \land φ))) \to (y = s \to \exists z (z = t \land φ))$
22	20 21	mpan	$⊢ \exists y (y = s \land \exists z (z = t \land φ)) \to (y = s \to \exists z (z = t \land φ))$
23		euequ	$⊢ \exists! z z = t$
24		eupick	$⊢ (\exists! z z = t \land \exists z (z = t \land φ)) \to (z = t \to φ)$
25	23 24	mpan	$⊢ \exists z (z = t \land φ) \to (z = t \to φ)$
26	22 25	syl6	$⊢ \exists y (y = s \land \exists z (z = t \land φ)) \to (y = s \to (z = t \to φ))$
27	19 26	syl6	$⊢ \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ))) \to (x = r \to (y = s \to (z = t \to φ)))$
28	27	3impd	$⊢ \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ))) \to ((x = r \land y = s \land z = t) \to φ)$
29	16 28	biimtrid	$⊢ \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ))) \to (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \to φ)$
30		df-3an	$⊢ (x = r \land y = s \land z = t) \leftrightarrow ((x = r \land y = s) \land z = t)$
31	16 30	bitri	$⊢ ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \leftrightarrow ((x = r \land y = s) \land z = t)$
32	31	anbi1i	$⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \leftrightarrow (((x = r \land y = s) \land z = t) \land φ)$
33		anass	$⊢ (((x = r \land y = s) \land z = t) \land φ) \leftrightarrow ((x = r \land y = s) \land (z = t \land φ))$
34		anass	$⊢ ((x = r \land y = s) \land (z = t \land φ)) \leftrightarrow (x = r \land (y = s \land (z = t \land φ)))$
35	32 33 34	3bitri	$⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \leftrightarrow (x = r \land (y = s \land (z = t \land φ)))$
36	35	3exbii	$⊢ \exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \leftrightarrow \exists x \exists y \exists z (x = r \land (y = s \land (z = t \land φ)))$
37		nfe1	$⊢ Ⅎ x \exists x (x = r \land \exists z (y = s \land (z = t \land φ)))$
38		19.8a	$⊢ (y = s \land (z = t \land φ)) \to \exists z (y = s \land (z = t \land φ))$
39	38	anim2i	$⊢ (x = r \land (y = s \land (z = t \land φ))) \to (x = r \land \exists z (y = s \land (z = t \land φ)))$
40	39	eximi	$⊢ \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists z (x = r \land \exists z (y = s \land (z = t \land φ)))$
41		biidd	$⊢ \forall x x = z \to ((x = r \land \exists z (y = s \land (z = t \land φ))) \leftrightarrow (x = r \land \exists z (y = s \land (z = t \land φ))))$
42	41	drex1v	$⊢ \forall x x = z \to (\exists x (x = r \land \exists z (y = s \land (z = t \land φ))) \leftrightarrow \exists z (x = r \land \exists z (y = s \land (z = t \land φ))))$
43	40 42	imbitrrid	$⊢ \forall x x = z \to (\exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists z (y = s \land (z = t \land φ))))$
44		19.40	$⊢ \exists z (x = r \land (y = s \land (z = t \land φ))) \to (\exists z x = r \land \exists z (y = s \land (z = t \land φ)))$
45		nfvd	$⊢ \neg \forall x x = z \to Ⅎ z x = r$
46	45	19.9d	$⊢ \neg \forall x x = z \to (\exists z x = r \to x = r)$
47	46	anim1d	$⊢ \neg \forall x x = z \to ((\exists z x = r \land \exists z (y = s \land (z = t \land φ))) \to (x = r \land \exists z (y = s \land (z = t \land φ))))$
48		19.8a	$⊢ (x = r \land \exists z (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists z (y = s \land (z = t \land φ)))$
49	44 47 48	syl56	$⊢ \neg \forall x x = z \to (\exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists z (y = s \land (z = t \land φ))))$
50	43 49	pm2.61i	$⊢ \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists z (y = s \land (z = t \land φ)))$
51	37 50	exlimi	$⊢ \exists x \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists z (y = s \land (z = t \land φ)))$
52	51	eximi	$⊢ \exists y \exists x \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists y \exists x (x = r \land \exists z (y = s \land (z = t \land φ)))$
53		excom	$⊢ \exists x \exists y \exists z (x = r \land (y = s \land (z = t \land φ))) \leftrightarrow \exists y \exists x \exists z (x = r \land (y = s \land (z = t \land φ)))$
54		excom	$⊢ \exists x \exists y (x = r \land \exists z (y = s \land (z = t \land φ))) \leftrightarrow \exists y \exists x (x = r \land \exists z (y = s \land (z = t \land φ)))$
55	52 53 54	3imtr4i	$⊢ \exists x \exists y \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists x \exists y (x = r \land \exists z (y = s \land (z = t \land φ)))$
56		nfe1	$⊢ Ⅎ x \exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ)))$
57		19.8a	$⊢ \exists z (y = s \land (z = t \land φ)) \to \exists y \exists z (y = s \land (z = t \land φ))$
58	57	anim2i	$⊢ (x = r \land \exists z (y = s \land (z = t \land φ))) \to (x = r \land \exists y \exists z (y = s \land (z = t \land φ)))$
59	58	eximi	$⊢ \exists y (x = r \land \exists z (y = s \land (z = t \land φ))) \to \exists y (x = r \land \exists y \exists z (y = s \land (z = t \land φ)))$
60		biidd	$⊢ \forall x x = y \to ((x = r \land \exists y \exists z (y = s \land (z = t \land φ))) \leftrightarrow (x = r \land \exists y \exists z (y = s \land (z = t \land φ))))$
61	60	drex1v	$⊢ \forall x x = y \to (\exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ))) \leftrightarrow \exists y (x = r \land \exists y \exists z (y = s \land (z = t \land φ))))$
62	59 61	imbitrrid	$⊢ \forall x x = y \to (\exists y (x = r \land \exists z (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ))))$
63		19.40	$⊢ \exists y (x = r \land \exists z (y = s \land (z = t \land φ))) \to (\exists y x = r \land \exists y \exists z (y = s \land (z = t \land φ)))$
64		nfvd	$⊢ \neg \forall x x = y \to Ⅎ y x = r$
65	64	19.9d	$⊢ \neg \forall x x = y \to (\exists y x = r \to x = r)$
66	65	anim1d	$⊢ \neg \forall x x = y \to ((\exists y x = r \land \exists y \exists z (y = s \land (z = t \land φ))) \to (x = r \land \exists y \exists z (y = s \land (z = t \land φ))))$
67		19.8a	$⊢ (x = r \land \exists y \exists z (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ)))$
68	63 66 67	syl56	$⊢ \neg \forall x x = y \to (\exists y (x = r \land \exists z (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ))))$
69	62 68	pm2.61i	$⊢ \exists y (x = r \land \exists z (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ)))$
70	56 69	exlimi	$⊢ \exists x \exists y (x = r \land \exists z (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ)))$
71		nfe1	$⊢ Ⅎ y \exists y (y = s \land \exists z (z = t \land φ))$
72		19.8a	$⊢ (z = t \land φ) \to \exists z (z = t \land φ)$
73	72	anim2i	$⊢ (y = s \land (z = t \land φ)) \to (y = s \land \exists z (z = t \land φ))$
74	73	eximi	$⊢ \exists z (y = s \land (z = t \land φ)) \to \exists z (y = s \land \exists z (z = t \land φ))$
75		biidd	$⊢ \forall y y = z \to ((y = s \land \exists z (z = t \land φ)) \leftrightarrow (y = s \land \exists z (z = t \land φ)))$
76	75	drex1v	$⊢ \forall y y = z \to (\exists y (y = s \land \exists z (z = t \land φ)) \leftrightarrow \exists z (y = s \land \exists z (z = t \land φ)))$
77	74 76	imbitrrid	$⊢ \forall y y = z \to (\exists z (y = s \land (z = t \land φ)) \to \exists y (y = s \land \exists z (z = t \land φ)))$
78		19.40	$⊢ \exists z (y = s \land (z = t \land φ)) \to (\exists z y = s \land \exists z (z = t \land φ))$
79		nfvd	$⊢ \neg \forall y y = z \to Ⅎ z y = s$
80	79	19.9d	$⊢ \neg \forall y y = z \to (\exists z y = s \to y = s)$
81	80	anim1d	$⊢ \neg \forall y y = z \to ((\exists z y = s \land \exists z (z = t \land φ)) \to (y = s \land \exists z (z = t \land φ)))$
82		19.8a	$⊢ (y = s \land \exists z (z = t \land φ)) \to \exists y (y = s \land \exists z (z = t \land φ))$
83	78 81 82	syl56	$⊢ \neg \forall y y = z \to (\exists z (y = s \land (z = t \land φ)) \to \exists y (y = s \land \exists z (z = t \land φ)))$
84	77 83	pm2.61i	$⊢ \exists z (y = s \land (z = t \land φ)) \to \exists y (y = s \land \exists z (z = t \land φ))$
85	71 84	exlimi	$⊢ \exists y \exists z (y = s \land (z = t \land φ)) \to \exists y (y = s \land \exists z (z = t \land φ))$
86	85	anim2i	$⊢ (x = r \land \exists y \exists z (y = s \land (z = t \land φ))) \to (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))$
87	86	eximi	$⊢ \exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))$
88	55 70 87	3syl	$⊢ \exists x \exists y \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))$
89	36 88	sylbi	$⊢ \exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \to \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))$
90	29 89	syl11	$⊢ ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \to (\exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \to φ)$
91		eqeq1	$⊢ w = ⟨⟨r, s⟩, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨⟨r, s⟩, t⟩ = ⟨⟨x, y⟩, z⟩)$
92		eqcom	$⊢ ⟨⟨r, s⟩, t⟩ = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩$
93	91 92	bitrdi	$⊢ w = ⟨⟨r, s⟩, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩)$
94	93	anbi1d	$⊢ w = ⟨⟨r, s⟩, t⟩ \to ((w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ))$
95	94	3exbidv	$⊢ w = ⟨⟨r, s⟩, t⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ))$
96	95	imbi1d	$⊢ w = ⟨⟨r, s⟩, t⟩ \to ((\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ) \leftrightarrow (\exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \to φ))$
97	93 96	imbi12d	$⊢ w = ⟨⟨r, s⟩, t⟩ \to ((w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)) \leftrightarrow (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \to (\exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \to φ)))$
98	90 97	mpbiri	$⊢ w = ⟨⟨r, s⟩, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ))$
99	15 98	syl6bi	$⊢ a = ⟨r, s⟩ \to (w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
100	99	adantr	$⊢ (a = ⟨r, s⟩ \land ⟨r, s⟩ = ⟨x, y⟩) \to (w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
101	100	exlimivv	$⊢ \exists r \exists s (a = ⟨r, s⟩ \land ⟨r, s⟩ = ⟨x, y⟩) \to (w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
102	13 101	sylbi	$⊢ a = ⟨x, y⟩ \to (w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
103	102	com3l	$⊢ w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (a = ⟨x, y⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
104	10 103	mpdd	$⊢ w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ))$
105	104	adantr	$⊢ (w = ⟨a, t⟩ \land ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩) \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ))$
106	105	exlimivv	$⊢ \exists a \exists t (w = ⟨a, t⟩ \land ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩) \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ))$
107	5 106	mpcom	$⊢ w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)$
108		19.8a	$⊢ (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
109		19.8a	$⊢ \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
110		19.8a	$⊢ \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
111	108 109 110	3syl	$⊢ (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
112	111	ex	$⊢ w = ⟨⟨x, y⟩, z⟩ \to (φ \to \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ))$
113	107 112	impbid	$⊢ w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow φ)$
114		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\}$
115	1 113 114	elab2	$⊢ ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow φ$

Metamath Proof Explorer

Theorem oprabidw

Proof