Theorem elxp5 7916

Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7915 when the double intersection does not create class existence problems (caused by int0 4928). (Contributed by NM, 1-Aug-2004.)

Assertion

Ref	Expression
elxp5	⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))

Proof of Theorem elxp5

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 5682	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
2		sneq 4601	. . . . . . . . . . . 12 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
3	2	rneqd 5926	. . . . . . . . . . 11 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
4	3	unieqd 4886	. . . . . . . . . 10 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ∪ ran {𝐴} = ∪ ran {⟨𝑥, 𝑦⟩})
5		vex 3467	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
6		vex 3467	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
7	5, 6	op2nda 6227	. . . . . . . . . 10 ⊢ ∪ ran {⟨𝑥, 𝑦⟩} = 𝑦
8	4, 7	eqtr2di 2821	. . . . . . . . 9 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ∪ ran {𝐴})
9	8	pm4.71ri 569	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
10	9	anbi1i 635	. . . . . . 7 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
11		anass 473	. . . . . . 7 ⊢ (((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
12	10, 11	bitri 278	. . . . . 6 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
13	12	exbii 1875	. . . . 5 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
14		snex 5408	. . . . . . . 8 ⊢ {𝐴} ∈ V
15	14	rnex 7903	. . . . . . 7 ⊢ ran {𝐴} ∈ V
16	15	uniex 7736	. . . . . 6 ⊢ ∪ ran {𝐴} ∈ V
17		opeq2 4840	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∪ ran {𝐴}⟩)
18	17	eqeq2d 2780	. . . . . . 7 ⊢ (𝑦 = ∪ ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
19		eleq1 2857	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → (𝑦 ∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶))
20	19	anbi2d 641	. . . . . . 7 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
21	18, 20	anbi12d 643	. . . . . 6 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
22	16, 21	ceqsexv 3511	. . . . 5 ⊢ (∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
23	13, 22	bitri 278	. . . 4 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
24		inteq 4916	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∩ 𝐴 = ∩ ⟨𝑥, ∪ ran {𝐴}⟩)
25	24	inteqd 4918	. . . . . . 7 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∩ ∩ 𝐴 = ∩ ∩ ⟨𝑥, ∪ ran {𝐴}⟩)
26	5, 16	op1stb 5451	. . . . . . 7 ⊢ ∩ ∩ ⟨𝑥, ∪ ran {𝐴}⟩ = 𝑥
27	25, 26	eqtr2di 2821	. . . . . 6 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → 𝑥 = ∩ ∩ 𝐴)
28	27	pm4.71ri 569	. . . . 5 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ (𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
29	28	anbi1i 635	. . . 4 ⊢ ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
30		anass 473	. . . 4 ⊢ (((𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
31	23, 29, 30	3bitri 300	. . 3 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
32	31	exbii 1875	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
33		eqvisset 3483	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → ∩ ∩ 𝐴 ∈ V)
34	33	adantr 485	. . . 4 ⊢ ((𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V)
35	34	exlimiv 1957	. . 3 ⊢ (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V)
36		elex 3484	. . . 4 ⊢ (∩ ∩ 𝐴 ∈ 𝐵 → ∩ ∩ 𝐴 ∈ V)
37	36	ad2antrl 740	. . 3 ⊢ ((𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) → ∩ ∩ 𝐴 ∈ V)
38		opeq1 4839	. . . . . 6 ⊢ (𝑥 = ∩ ∩ 𝐴 → ⟨𝑥, ∪ ran {𝐴}⟩ = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩)
39	38	eqeq2d 2780	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ 𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩))
40		eleq1 2857	. . . . . 6 ⊢ (𝑥 = ∩ ∩ 𝐴 → (𝑥 ∈ 𝐵 ↔ ∩ ∩ 𝐴 ∈ 𝐵))
41	40	anbi1d 642	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → ((𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶) ↔ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
42	39, 41	anbi12d 643	. . . 4 ⊢ (𝑥 = ∩ ∩ 𝐴 → ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
43	42	ceqsexgv 3622	. . 3 ⊢ (∩ ∩ 𝐴 ∈ V → (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
44	35, 37, 43	pm5.21nii 381	. 2 ⊢ (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
45	1, 32, 44	3bitri 300	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3463  {csn 4591  ⟨cop 4597  ∪ cuni 4873  ∩ cint 4913   × cxp 5657  ran crn 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-int 4914  df-br 5111  df-opab 5175  df-xp 5665  df-rel 5666  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by: (None)