Theorem elxp5 7922

Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7921 when the double intersection does not create class existence problems (caused by int0 4929). (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 5686	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
2		sneq 4601	. . . . . . . . . . . 12 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
3	2	rneqd 5930	. . . . . . . . . . 11 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
4	3	unieqd 4887	. . . . . . . . . 10 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ∪ ran {𝐴} = ∪ ran {⟨𝑥, 𝑦⟩})
5		vex 3461	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
6		vex 3461	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
7	5, 6	op2nda 6231	. . . . . . . . . 10 ⊢ ∪ ran {⟨𝑥, 𝑦⟩} = 𝑦
8	4, 7	eqtr2di 2817	. . . . . . . . 9 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ∪ ran {𝐴})
9	8	pm4.71ri 570	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
10	9	anbi1i 636	. . . . . . 7 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
11		anass 474	. . . . . . 7 ⊢ (((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
12	10, 11	bitri 278	. . . . . 6 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
13	12	exbii 1881	. . . . 5 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
14		snex 5412	. . . . . . . 8 ⊢ {𝐴} ∈ V
15	14	rnex 7909	. . . . . . 7 ⊢ ran {𝐴} ∈ V
16	15	uniex 7745	. . . . . 6 ⊢ ∪ ran {𝐴} ∈ V
17		opeq2 4841	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∪ ran {𝐴}⟩)
18	17	eqeq2d 2776	. . . . . . 7 ⊢ (𝑦 = ∪ ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
19		eleq1 2853	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → (𝑦 ∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶))
20	19	anbi2d 642	. . . . . . 7 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
21	18, 20	anbi12d 644	. . . . . 6 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
22	16, 21	ceqsexv 3505	. . . . 5 ⊢ (∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
23	13, 22	bitri 278	. . . 4 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
24		inteq 4917	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∩ 𝐴 = ∩ ⟨𝑥, ∪ ran {𝐴}⟩)
25	24	inteqd 4919	. . . . . . 7 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∩ ∩ 𝐴 = ∩ ∩ ⟨𝑥, ∪ ran {𝐴}⟩)
26	5, 16	op1stb 5455	. . . . . . 7 ⊢ ∩ ∩ ⟨𝑥, ∪ ran {𝐴}⟩ = 𝑥
27	25, 26	eqtr2di 2817	. . . . . 6 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → 𝑥 = ∩ ∩ 𝐴)
28	27	pm4.71ri 570	. . . . 5 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ (𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
29	28	anbi1i 636	. . . 4 ⊢ ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
30		anass 474	. . . 4 ⊢ (((𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
31	23, 29, 30	3bitri 300	. . 3 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
32	31	exbii 1881	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
33		eqvisset 3477	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → ∩ ∩ 𝐴 ∈ V)
34	33	adantr 486	. . . 4 ⊢ ((𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V)
35	34	exlimiv 1963	. . 3 ⊢ (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V)
36		elex 3478	. . . 4 ⊢ (∩ ∩ 𝐴 ∈ 𝐵 → ∩ ∩ 𝐴 ∈ V)
37	36	ad2antrl 741	. . 3 ⊢ ((𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) → ∩ ∩ 𝐴 ∈ V)
38		opeq1 4840	. . . . . 6 ⊢ (𝑥 = ∩ ∩ 𝐴 → ⟨𝑥, ∪ ran {𝐴}⟩ = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩)
39	38	eqeq2d 2776	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ 𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩))
40		eleq1 2853	. . . . . 6 ⊢ (𝑥 = ∩ ∩ 𝐴 → (𝑥 ∈ 𝐵 ↔ ∩ ∩ 𝐴 ∈ 𝐵))
41	40	anbi1d 643	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → ((𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶) ↔ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
42	39, 41	anbi12d 644	. . . 4 ⊢ (𝑥 = ∩ ∩ 𝐴 → ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
43	42	ceqsexgv 3615	. . 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 {𝐴} ∈ 𝐶)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3457  {csn 4591  ⟨cop 4597  ∪ cuni 4874  ∩ cint 4914   × cxp 5661  ran crn 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by: (None)