Theorem elxp5 7004

Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7003 when the double intersection does not create class existence problems (caused by int0 4425). (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 5055	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
2		sneq 4135	. . . . . . . . . . . 12 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
3	2	rneqd 5274	. . . . . . . . . . 11 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
4	3	unieqd 4382	. . . . . . . . . 10 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ∪ ran {𝐴} = ∪ ran {⟨𝑥, 𝑦⟩})
5		vex 3176	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
6		vex 3176	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
7	5, 6	op2nda 5538	. . . . . . . . . 10 ⊢ ∪ ran {⟨𝑥, 𝑦⟩} = 𝑦
8	4, 7	syl6req 2661	. . . . . . . . 9 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ∪ ran {𝐴})
9	8	pm4.71ri 663	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
10	9	anbi1i 727	. . . . . . 7 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
11		anass 679	. . . . . . 7 ⊢ (((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
12	10, 11	bitri 263	. . . . . 6 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
13	12	exbii 1764	. . . . 5 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
14		snex 4835	. . . . . . . 8 ⊢ {𝐴} ∈ V
15	14	rnex 6992	. . . . . . 7 ⊢ ran {𝐴} ∈ V
16	15	uniex 6851	. . . . . 6 ⊢ ∪ ran {𝐴} ∈ V
17		opeq2 4341	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∪ ran {𝐴}⟩)
18	17	eqeq2d 2620	. . . . . . 7 ⊢ (𝑦 = ∪ ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
19		eleq1 2676	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → (𝑦 ∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶))
20	19	anbi2d 736	. . . . . . 7 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
21	18, 20	anbi12d 743	. . . . . 6 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
22	16, 21	ceqsexv 3215	. . . . 5 ⊢ (∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
23	13, 22	bitri 263	. . . 4 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
24		inteq 4413	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∩ 𝐴 = ∩ ⟨𝑥, ∪ ran {𝐴}⟩)
25	24	inteqd 4415	. . . . . . 7 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∩ ∩ 𝐴 = ∩ ∩ ⟨𝑥, ∪ ran {𝐴}⟩)
26	5, 16	op1stb 4867	. . . . . . 7 ⊢ ∩ ∩ ⟨𝑥, ∪ ran {𝐴}⟩ = 𝑥
27	25, 26	syl6req 2661	. . . . . 6 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → 𝑥 = ∩ ∩ 𝐴)
28	27	pm4.71ri 663	. . . . 5 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ (𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
29	28	anbi1i 727	. . . 4 ⊢ ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
30		anass 679	. . . 4 ⊢ (((𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
31	23, 29, 30	3bitri 285	. . 3 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
32	31	exbii 1764	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
33		eqvisset 3184	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → ∩ ∩ 𝐴 ∈ V)
34	33	adantr 480	. . . 4 ⊢ ((𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V)
35	34	exlimiv 1845	. . 3 ⊢ (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V)
36		elex 3185	. . . 4 ⊢ (∩ ∩ 𝐴 ∈ 𝐵 → ∩ ∩ 𝐴 ∈ V)
37	36	ad2antrl 760	. . 3 ⊢ ((𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) → ∩ ∩ 𝐴 ∈ V)
38		opeq1 4340	. . . . . 6 ⊢ (𝑥 = ∩ ∩ 𝐴 → ⟨𝑥, ∪ ran {𝐴}⟩ = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩)
39	38	eqeq2d 2620	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ 𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩))
40		eleq1 2676	. . . . . 6 ⊢ (𝑥 = ∩ ∩ 𝐴 → (𝑥 ∈ 𝐵 ↔ ∩ ∩ 𝐴 ∈ 𝐵))
41	40	anbi1d 737	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → ((𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶) ↔ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
42	39, 41	anbi12d 743	. . . 4 ⊢ (𝑥 = ∩ ∩ 𝐴 → ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
43	42	ceqsexgv 3305	. . 3 ⊢ (∩ ∩ 𝐴 ∈ V → (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
44	35, 37, 43	pm5.21nii 367	. 2 ⊢ (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
45	1, 32, 44	3bitri 285	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))

Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173  {csn 4125  ⟨cop 4131  ∪ cuni 4372  ∩ cint 4410   × cxp 5036  ran crn 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-int 4411  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-cnv 5046  df-dm 5048  df-rn 5049

This theorem is referenced by: (None)