Theorem oprabid 5457

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 1376 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 2534	. . . 4 ⊢ x ∈ V
2		vex 2534	. . . 4 ⊢ y ∈ V
3	1, 2	opex 3936	. . 3 ⊢ ⟨x, y⟩ ∈ V
4		vex 2534	. . 3 ⊢ z ∈ V
5		opexg 3934	. . 3 ⊢ ((⟨x, y⟩ ∈ V ∧ z ∈ V) → ⟨⟨x, y⟩, z⟩ ∈ V)
6	3, 4, 5	mp2an 404	. 2 ⊢ ⟨⟨x, y⟩, z⟩ ∈ V
7	3, 4	eqvinop 3950	. . . . 5 ⊢ (w = ⟨⟨x, y⟩, z⟩ ↔ ∃𝑎∃𝑡(w = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩))
8	7	biimpi 113	. . . 4 ⊢ (w = ⟨⟨x, y⟩, z⟩ → ∃𝑎∃𝑡(w = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩))
9		eqeq1 2024	. . . . . . . 8 ⊢ (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ ↔ ⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩))
10		vex 2534	. . . . . . . . 9 ⊢ 𝑎 ∈ V
11		vex 2534	. . . . . . . . 9 ⊢ 𝑡 ∈ V
12	10, 11	opth1 3943	. . . . . . . 8 ⊢ (⟨𝑎, 𝑡⟩ = ⟨⟨x, y⟩, z⟩ → 𝑎 = ⟨x, y⟩)
13	9, 12	syl6bi 152	. . . . . . 7 ⊢ (w = ⟨𝑎, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ → 𝑎 = ⟨x, y⟩))
14	1, 2	eqvinop 3950	. . . . . . . . 9 ⊢ (𝑎 = ⟨x, y⟩ ↔ ∃𝑟∃𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨x, y⟩))
15		opeq1 3519	. . . . . . . . . . . . 13 ⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → ⟨𝑎, 𝑡⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
16	15	eqeq2d 2029	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → (w = ⟨𝑎, 𝑡⟩ ↔ w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
17	1, 2, 4	otth2 3948	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ (x = 𝑟 ∧ y = 𝑠 ∧ z = 𝑡))
18		df-3an 873	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x = 𝑟 ∧ y = 𝑠 ∧ z = 𝑡) ↔ ((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡))
19	17, 18	bitri 173	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ ((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡))
20	19	anbi1i 434	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) ↔ (((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡) ∧ φ))
21		anass 383	. . . . . . . . . . . . . . . . 17 ⊢ ((((x = 𝑟 ∧ y = 𝑠) ∧ z = 𝑡) ∧ φ) ↔ ((x = 𝑟 ∧ y = 𝑠) ∧ (z = 𝑡 ∧ φ)))
22		anass 383	. . . . . . . . . . . . . . . . 17 ⊢ (((x = 𝑟 ∧ y = 𝑠) ∧ (z = 𝑡 ∧ φ)) ↔ (x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
23	20, 21, 22	3bitri 195	. . . . . . . . . . . . . . . 16 ⊢ ((⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) ↔ (x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
24	23	3exbii 1476	. . . . . . . . . . . . . . 15 ⊢ (∃x∃y∃z(⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ) ↔ ∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
25		oprabidlem 5456	. . . . . . . . . . . . . . . . . 18 ⊢ (∃x∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
26	25	eximi 1469	. . . . . . . . . . . . . . . . 17 ⊢ (∃y∃x∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃y∃x(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
27		excom 1532	. . . . . . . . . . . . . . . . 17 ⊢ (∃x∃y∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))) ↔ ∃y∃x∃z(x = 𝑟 ∧ (y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
28		excom 1532	. . . . . . . . . . . . . . . . 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 5456	. . . . . . . . . . . . . . . 16 ⊢ (∃x∃y(x = 𝑟 ∧ ∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))) → ∃x(x = 𝑟 ∧ ∃y∃z(y = 𝑠 ∧ (z = 𝑡 ∧ φ))))
31		oprabidlem 5456	. . . . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . . 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 1973	. . . . . . . . . . . . . . . . . . 19 ⊢ ∃!x x = 𝑟
37		eupick 1957	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃!x x = 𝑟 ∧ ∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)))) → (x = 𝑟 → ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))))
38	36, 37	mpan 402	. . . . . . . . . . . . . . . . . 18 ⊢ (∃x(x = 𝑟 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (x = 𝑟 → ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))))
39		euequ1 1973	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∃!y y = 𝑠
40		eupick 1957	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃!y y = 𝑠 ∧ ∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ))) → (y = 𝑠 → ∃z(z = 𝑡 ∧ φ)))
41	39, 40	mpan 402	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃y(y = 𝑠 ∧ ∃z(z = 𝑡 ∧ φ)) → (y = 𝑠 → ∃z(z = 𝑡 ∧ φ)))
42		euequ1 1973	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∃!z z = 𝑡
43		eupick 1957	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∃!z z = 𝑡 ∧ ∃z(z = 𝑡 ∧ φ)) → (z = 𝑡 → φ))
44	42, 43	mpan 402	. . . . . . . . . . . . . . . . . . 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 1102	. . . . . . . . . . . . . . . 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 2024	. . . . . . . . . . . . . . 15 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ ↔ ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨x, y⟩, z⟩))
52		eqcom 2020	. . . . . . . . . . . . . . 15 ⊢ (⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨x, y⟩, z⟩ ↔ ⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
53	51, 52	syl6bb 185	. . . . . . . . . . . . . 14 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (w = ⟨⟨x, y⟩, z⟩ ↔ ⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
54	53	anbi1d 441	. . . . . . . . . . . . . . . 16 ⊢ (w = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((w = ⟨⟨x, y⟩, z⟩ ∧ φ) ↔ (⟨⟨x, y⟩, z⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ φ)))
55	54	3exbidv 1727	. . . . . . . . . . . . . . 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 1754	. . . . . . . . 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 1754	. . . 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 1460	. . . . 5 ⊢ ((w = ⟨⟨x, y⟩, z⟩ ∧ φ) → ∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ))
69		19.8a 1460	. . . . 5 ⊢ (∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ) → ∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ))
70		19.8a 1460	. . . . 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 5436	. 2 ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {w ∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)}
75	6, 73, 74	elab2 2663	1 ⊢ (⟨⟨x, y⟩, z⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ φ)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 871   = wceq 1226  ∃wex 1358   ∈ wcel 1370  ∃!weu 1878  Vcvv 2531  ⟨cop 3349  {coprab 5433

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 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914  ax-setind 4200

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-fal 1232  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ne 2184  df-ral 2285  df-v 2533  df-dif 2893  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-oprab 5436

This theorem is referenced by:  ssoprab2b  5481  ovid  5536  ovidig  5537  tposoprab  5813