Theorem otsnelsi3 5806

Description: Ordered triple membership in triple singleton image. (Contributed by SF, 12-Feb-2015.)

Hypotheses

Ref	Expression
otsnelsi3.1	⊢ A ∈ V
otsnelsi3.2	⊢ B ∈ V
otsnelsi3.3	⊢ C ∈ V

Assertion

Ref	Expression
otsnelsi3	⊢ (⟨{A}, ⟨{B}, {C}⟩⟩ ∈ SI3 R ↔ ⟨A, ⟨B, C⟩⟩ ∈ R)

Proof of Theorem otsnelsi3

Dummy variables p x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-si3 5759	. . 3 ⊢ SI3 R = (( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) “ ℘1R)
2	1	eleq2i 2417	. 2 ⊢ (⟨{A}, ⟨{B}, {C}⟩⟩ ∈ SI3 R ↔ ⟨{A}, ⟨{B}, {C}⟩⟩ ∈ (( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) “ ℘1R))
3		elimapw1 4945	. 2 ⊢ (⟨{A}, ⟨{B}, {C}⟩⟩ ∈ (( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) “ ℘1R) ↔ ∃p ∈ R ⟨{p}, ⟨{A}, ⟨{B}, {C}⟩⟩⟩ ∈ ( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))))
4		oteltxp 5783	. . . . 5 ⊢ (⟨{p}, ⟨{A}, ⟨{B}, {C}⟩⟩⟩ ∈ ( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) ↔ (⟨{p}, {A}⟩ ∈ SI 1st ∧ ⟨{p}, ⟨{B}, {C}⟩⟩ ∈ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))))
5		vex 2863	. . . . . . . 8 ⊢ p ∈ V
6		otsnelsi3.1	. . . . . . . 8 ⊢ A ∈ V
7	5, 6	opsnelsi 5775	. . . . . . 7 ⊢ (⟨{p}, {A}⟩ ∈ SI 1st ↔ ⟨p, A⟩ ∈ 1st )
8		df-br 4641	. . . . . . 7 ⊢ (p1st A ↔ ⟨p, A⟩ ∈ 1st )
9	7, 8	bitr4i 243	. . . . . 6 ⊢ (⟨{p}, {A}⟩ ∈ SI 1st ↔ p1st A)
10		oteltxp 5783	. . . . . . 7 ⊢ (⟨{p}, ⟨{B}, {C}⟩⟩ ∈ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd )) ↔ (⟨{p}, {B}⟩ ∈ SI (1st ∘ 2nd ) ∧ ⟨{p}, {C}⟩ ∈ SI (2nd ∘ 2nd )))
11		otsnelsi3.2	. . . . . . . . . 10 ⊢ B ∈ V
12	5, 11	opsnelsi 5775	. . . . . . . . 9 ⊢ (⟨{p}, {B}⟩ ∈ SI (1st ∘ 2nd ) ↔ ⟨p, B⟩ ∈ (1st ∘ 2nd ))
13		opelco 4885	. . . . . . . . 9 ⊢ (⟨p, B⟩ ∈ (1st ∘ 2nd ) ↔ ∃x(p2nd x ∧ x1st B))
14		opeq 4620	. . . . . . . . . . . . . 14 ⊢ p = ⟨ Proj1 p, Proj2 p⟩
15	14	breq1i 4647	. . . . . . . . . . . . 13 ⊢ (p2nd x ↔ ⟨ Proj1 p, Proj2 p⟩2nd x)
16	5	proj1ex 4594	. . . . . . . . . . . . . 14 ⊢ Proj1 p ∈ V
17	5	proj2ex 4595	. . . . . . . . . . . . . 14 ⊢ Proj2 p ∈ V
18	16, 17	opbr2nd 5503	. . . . . . . . . . . . 13 ⊢ (⟨ Proj1 p, Proj2 p⟩2nd x ↔ Proj2 p = x)
19		eqcom 2355	. . . . . . . . . . . . 13 ⊢ ( Proj2 p = x ↔ x = Proj2 p)
20	15, 18, 19	3bitri 262	. . . . . . . . . . . 12 ⊢ (p2nd x ↔ x = Proj2 p)
21	20	anbi1i 676	. . . . . . . . . . 11 ⊢ ((p2nd x ∧ x1st B) ↔ (x = Proj2 p ∧ x1st B))
22	21	exbii 1582	. . . . . . . . . 10 ⊢ (∃x(p2nd x ∧ x1st B) ↔ ∃x(x = Proj2 p ∧ x1st B))
23		breq1 4643	. . . . . . . . . . 11 ⊢ (x = Proj2 p → (x1st B ↔ Proj2 p1st B))
24	17, 23	ceqsexv 2895	. . . . . . . . . 10 ⊢ (∃x(x = Proj2 p ∧ x1st B) ↔ Proj2 p1st B)
25	22, 24	bitri 240	. . . . . . . . 9 ⊢ (∃x(p2nd x ∧ x1st B) ↔ Proj2 p1st B)
26	12, 13, 25	3bitri 262	. . . . . . . 8 ⊢ (⟨{p}, {B}⟩ ∈ SI (1st ∘ 2nd ) ↔ Proj2 p1st B)
27		otsnelsi3.3	. . . . . . . . . 10 ⊢ C ∈ V
28	5, 27	opsnelsi 5775	. . . . . . . . 9 ⊢ (⟨{p}, {C}⟩ ∈ SI (2nd ∘ 2nd ) ↔ ⟨p, C⟩ ∈ (2nd ∘ 2nd ))
29		opelco 4885	. . . . . . . . 9 ⊢ (⟨p, C⟩ ∈ (2nd ∘ 2nd ) ↔ ∃x(p2nd x ∧ x2nd C))
30	20	anbi1i 676	. . . . . . . . . . 11 ⊢ ((p2nd x ∧ x2nd C) ↔ (x = Proj2 p ∧ x2nd C))
31	30	exbii 1582	. . . . . . . . . 10 ⊢ (∃x(p2nd x ∧ x2nd C) ↔ ∃x(x = Proj2 p ∧ x2nd C))
32		breq1 4643	. . . . . . . . . . 11 ⊢ (x = Proj2 p → (x2nd C ↔ Proj2 p2nd C))
33	17, 32	ceqsexv 2895	. . . . . . . . . 10 ⊢ (∃x(x = Proj2 p ∧ x2nd C) ↔ Proj2 p2nd C)
34	31, 33	bitri 240	. . . . . . . . 9 ⊢ (∃x(p2nd x ∧ x2nd C) ↔ Proj2 p2nd C)
35	28, 29, 34	3bitri 262	. . . . . . . 8 ⊢ (⟨{p}, {C}⟩ ∈ SI (2nd ∘ 2nd ) ↔ Proj2 p2nd C)
36	26, 35	anbi12i 678	. . . . . . 7 ⊢ ((⟨{p}, {B}⟩ ∈ SI (1st ∘ 2nd ) ∧ ⟨{p}, {C}⟩ ∈ SI (2nd ∘ 2nd )) ↔ ( Proj2 p1st B ∧ Proj2 p2nd C))
37	16, 17	opbr2nd 5503	. . . . . . . 8 ⊢ (⟨ Proj1 p, Proj2 p⟩2nd ⟨B, C⟩ ↔ Proj2 p = ⟨B, C⟩)
38	14	breq1i 4647	. . . . . . . 8 ⊢ (p2nd ⟨B, C⟩ ↔ ⟨ Proj1 p, Proj2 p⟩2nd ⟨B, C⟩)
39	11, 27	op1st2nd 5791	. . . . . . . 8 ⊢ (( Proj2 p1st B ∧ Proj2 p2nd C) ↔ Proj2 p = ⟨B, C⟩)
40	37, 38, 39	3bitr4ri 269	. . . . . . 7 ⊢ (( Proj2 p1st B ∧ Proj2 p2nd C) ↔ p2nd ⟨B, C⟩)
41	10, 36, 40	3bitri 262	. . . . . 6 ⊢ (⟨{p}, ⟨{B}, {C}⟩⟩ ∈ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd )) ↔ p2nd ⟨B, C⟩)
42	9, 41	anbi12i 678	. . . . 5 ⊢ ((⟨{p}, {A}⟩ ∈ SI 1st ∧ ⟨{p}, ⟨{B}, {C}⟩⟩ ∈ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) ↔ (p1st A ∧ p2nd ⟨B, C⟩))
43	11, 27	opex 4589	. . . . . 6 ⊢ ⟨B, C⟩ ∈ V
44	6, 43	op1st2nd 5791	. . . . 5 ⊢ ((p1st A ∧ p2nd ⟨B, C⟩) ↔ p = ⟨A, ⟨B, C⟩⟩)
45	4, 42, 44	3bitri 262	. . . 4 ⊢ (⟨{p}, ⟨{A}, ⟨{B}, {C}⟩⟩⟩ ∈ ( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) ↔ p = ⟨A, ⟨B, C⟩⟩)
46	45	rexbii 2640	. . 3 ⊢ (∃p ∈ R ⟨{p}, ⟨{A}, ⟨{B}, {C}⟩⟩⟩ ∈ ( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) ↔ ∃p ∈ R p = ⟨A, ⟨B, C⟩⟩)
47		risset 2662	. . 3 ⊢ (⟨A, ⟨B, C⟩⟩ ∈ R ↔ ∃p ∈ R p = ⟨A, ⟨B, C⟩⟩)
48	46, 47	bitr4i 243	. 2 ⊢ (∃p ∈ R ⟨{p}, ⟨{A}, ⟨{B}, {C}⟩⟩⟩ ∈ ( SI 1st ⊗ ( SI (1st ∘ 2nd ) ⊗ SI (2nd ∘ 2nd ))) ↔ ⟨A, ⟨B, C⟩⟩ ∈ R)
49	2, 3, 48	3bitri 262	1 ⊢ (⟨{A}, ⟨{B}, {C}⟩⟩ ∈ SI3 R ↔ ⟨A, ⟨B, C⟩⟩ ∈ R)

Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2616  Vcvv 2860  {csn 3738  ℘₁cpw1 4136  ⟨cop 4562   Proj1 cproj1 4564   Proj2 cproj2 4565   class class class wbr 4640  1^st c1st 4718   SI csi 4721   ∘ ccom 4722   “ cima 4723  2^nd c2nd 4784   ⊗ ctxp 5736   SI₃ csi3 5758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-co 4727  df-ima 4728  df-si 4729  df-cnv 4786  df-2nd 4798  df-txp 5737  df-si3 5759

This theorem is referenced by:  composeex  5821  addcfnex  5825  funsex  5829  crossex  5851  domfnex  5871  ranfnex  5872  transex  5911  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  mucex  6134  ovcelem1  6172  ceex  6175