Theorem oprabid 5480

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Although this theorem would be useful with a distinct variable constraint between x, y, and z, we use ax-bnd 1396 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)

Assertion

Ref	Expression
oprabid	⊢ (⟨⟨x, y⟩, z⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ φ)

Proof of Theorem oprabid

Dummy variables 𝑎 𝑟 𝑠 𝑡 w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2554	. . . 4 ⊢ x ∈ V
2		vex 2554	. . . 4 ⊢ y ∈ V
3	1, 2	opex 3957	. . 3 ⊢ ⟨x, y⟩ ∈ V
4		vex 2554	. . 3 ⊢ z ∈ V
5		opexg 3955	. . 3 ⊢ ((⟨x, y⟩ ∈ V ∧ z ∈ V) → ⟨⟨x, y⟩, z⟩ ∈ V)
6	3, 4, 5	mp2an 402	. 2 ⊢ ⟨⟨x, y⟩, z⟩ ∈ V
7	3, 4	eqvinop 3971	. . . . 5 ⊢ (w = ⟨⟨x, y⟩, z⟩ ↔ ∃𝑎∃𝑡(w = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩))
8	7	biimpi 113	. . . 4 ⊢ (w = ⟨⟨x, y⟩, z⟩ → ∃𝑎∃𝑡(w = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩))
9		eqeq1 2043	. . . . . . . 8 ⊢ (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ ↔ ⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩))
10		vex 2554	. . . . . . . . 9 ⊢ 𝑎 ∈ V
11		vex 2554	. . . . . . . . 9 ⊢ 𝑡 ∈ V
12	10, 11	opth1 3964	. . . . . . . 8 ⊢ (⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩ → 𝑎 = ⟨x, y⟩)
13	9, 12	syl6bi 152	. . . . . . 7 ⊢ (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ → 𝑎 = ⟨x, y⟩))
14	1, 2	eqvinop 3971	. . . . . . . . 9 ⊢ (𝑎 = ⟨x, y⟩ ↔ ∃𝑟∃𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨x, y⟩))
15		opeq1 3540	. . . . . . . . . . . . 13 ⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → ⟨𝑎, 𝑡⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
16	15	eqeq2d 2048	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → (w = ⟨𝑎, 𝑡⟩ ↔ w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
17	1, 2, 4	otth2 3969	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ (x = 𝑟 ∧ y = 𝑠 ∧ z = 𝑡))
18		df-3an 886	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x = 𝑟 ∧ y = 𝑠 ∧ z = 𝑡) ↔ ((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡))
19	17, 18	bitri 173	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ ((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡))
20	19	anbi1i 431	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) ↔ (((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡) ∧ φ))
21		anass 381	. . . . . . . . . . . . . . . . 17 ⊢ ((((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡) ∧ φ) ↔ ((x = 𝑟 ∧ y = 𝑠) ∧ (z = 𝑡 ∧ φ)))
22		anass 381	. . . . . . . . . . . . . . . . 17 ⊢ (((x = 𝑟 ∧ y = 𝑠) ∧ (z = 𝑡 ∧ φ)) ↔ (x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
23	20, 21, 22	3bitri 195	. . . . . . . . . . . . . . . 16 ⊢ ((⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) ↔ (x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
24	23	3exbii 1495	. . . . . . . . . . . . . . 15 ⊢ (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) ↔ ∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
25		oprabidlem 5479	. . . . . . . . . . . . . . . . . 18 ⊢ (∃x∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
26	25	eximi 1488	. . . . . . . . . . . . . . . . 17 ⊢ (∃y∃x∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃y∃x(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
27		excom 1551	. . . . . . . . . . . . . . . . 17 ⊢ (∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) ↔ ∃y∃x∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
28		excom 1551	. . . . . . . . . . . . . . . . 17 ⊢ (∃x∃y(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))) ↔ ∃y∃x(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
29	26, 27, 28	3imtr4i 190	. . . . . . . . . . . . . . . 16 ⊢ (∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x∃y(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
30		oprabidlem 5479	. . . . . . . . . . . . . . . 16 ⊢ (∃x∃y(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃y∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
31		oprabidlem 5479	. . . . . . . . . . . . . . . . . 18 ⊢ (∃y∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ)) → ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))
32	31	anim2i 324	. . . . . . . . . . . . . . . . 17 ⊢ ((x = 𝑟 ∧ ∃y∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → (x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))))
33	32	eximi 1488	. . . . . . . . . . . . . . . 16 ⊢ (∃x(x = 𝑟 ∧ ∃y∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))))
34	29, 30, 33	3syl 17	. . . . . . . . . . . . . . 15 ⊢ (∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))))
35	24, 34	sylbi 114	. . . . . . . . . . . . . 14 ⊢ (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) → ∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))))
36		euequ1 1992	. . . . . . . . . . . . . . . . . . 19 ⊢ ∃!x x = 𝑟
37		eupick 1976	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃!x x = 𝑟 ∧ ∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))) → (x = 𝑟 → ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))))
38	36, 37	mpan 400	. . . . . . . . . . . . . . . . . 18 ⊢ (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (x = 𝑟 → ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))))
39		euequ1 1992	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∃!y y = 𝑠
40		eupick 1976	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃!y y = 𝑠 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (y = 𝑠 → ∃z(z = 𝑡 ∧ φ)))
41	39, 40	mpan 400	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)) → (y = 𝑠 → ∃z(z = 𝑡 ∧ φ)))
42		euequ1 1992	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∃!z z = 𝑡
43		eupick 1976	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃!z z = 𝑡 ∧ ∃z(z = 𝑡 ∧ φ)) → (z = 𝑡 → φ))
44	42, 43	mpan 400	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃z(z = 𝑡 ∧ φ) → (z = 𝑡 → φ))
45	41, 44	syl6 29	. . . . . . . . . . . . . . . . . 18 ⊢ (∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)) → (y = 𝑠 → (z = 𝑡 → φ)))
46	38, 45	syl6 29	. . . . . . . . . . . . . . . . 17 ⊢ (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (x = 𝑟 → (y = 𝑠 → (z = 𝑡 → φ))))
47	46	3impd 1117	. . . . . . . . . . . . . . . 16 ⊢ (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → ((x = 𝑟 ∧ y = 𝑠 ∧ z = 𝑡) → φ))
48	17, 47	syl5bi 141	. . . . . . . . . . . . . . 15 ⊢ (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → φ))
49	48	com12 27	. . . . . . . . . . . . . 14 ⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → φ))
50	35, 49	syl5 28	. . . . . . . . . . . . 13 ⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) → φ))
51		eqeq1 2043	. . . . . . . . . . . . . . 15 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ ↔ ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨x, y⟩, z⟩))
52		eqcom 2039	. . . . . . . . . . . . . . 15 ⊢ (⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨x, y⟩, z⟩ ↔ ⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
53	51, 52	syl6bb 185	. . . . . . . . . . . . . 14 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ ↔ ⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
54	53	anbi1d 438	. . . . . . . . . . . . . . . 16 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((w = ⟨⟨x, y⟩, z⟩ ∧ φ) ↔ (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ)))
55	54	3exbidv 1746	. . . . . . . . . . . . . . 15 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) ↔ ∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ)))
56	55	imbi1d 220	. . . . . . . . . . . . . 14 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ) ↔ (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) → φ)))
57	53, 56	imbi12d 223	. . . . . . . . . . . . 13 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ)) ↔ (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) → φ))))
58	50, 57	mpbiri 157	. . . . . . . . . . . 12 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ)))
59	16, 58	syl6bi 152	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ))))
60	59	adantr 261	. . . . . . . . . 10 ⊢ ((𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨x, y⟩) → (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ))))
61	60	exlimivv 1773	. . . . . . . . 9 ⊢ (∃𝑟∃𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨x, y⟩) → (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ))))
62	14, 61	sylbi 114	. . . . . . . 8 ⊢ (𝑎 = ⟨x, y⟩ → (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ))))
63	62	com3l 75	. . . . . . 7 ⊢ (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ → (𝑎 = ⟨x, y⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ))))
64	13, 63	mpdd 36	. . . . . 6 ⊢ (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ)))
65	64	adantr 261	. . . . 5 ⊢ ((w = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩) → (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ)))
66	65	exlimivv 1773	. . . 4 ⊢ (∃𝑎∃𝑡(w = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩) → (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ)))
67	8, 66	mpcom 32	. . 3 ⊢ (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → φ))
68		19.8a 1479	. . . . 5 ⊢ ((w = ⟨⟨x, y⟩, z⟩ ∧ φ) → ∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ))
69		19.8a 1479	. . . . 5 ⊢ (∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → ∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ))
70		19.8a 1479	. . . . 5 ⊢ (∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ))
71	68, 69, 70	3syl 17	. . . 4 ⊢ ((w = ⟨⟨x, y⟩, z⟩ ∧ φ) → ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ))
72	71	ex 108	. . 3 ⊢ (w = ⟨⟨x, y⟩, z⟩ → (φ → ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)))
73	67, 72	impbid 120	. 2 ⊢ (w = ⟨⟨x, y⟩, z⟩ → (∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) ↔ φ))
74		df-oprab 5459	. 2 ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {w ∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)}
75	6, 73, 74	elab2 2684	1 ⊢ (⟨⟨x, y⟩, z⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ φ)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∃!weu 1897  Vcvv 2551  ⟨cop 3370  {coprab 5456

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-oprab 5459

This theorem is referenced by:  ssoprab2b  5504  ovid  5559  ovidig  5560  tposoprab  5836  xpcomco  6236