Theorem elxp5 7931

Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7930 when the double intersection does not create class existence problems (caused by int0 4965). (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 5701	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
2		sneq 4639	. . . . . . . . . . . 12 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
3	2	rneqd 5940	. . . . . . . . . . 11 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
4	3	unieqd 4921	. . . . . . . . . 10 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ∪ ran {𝐴} = ∪ ran {⟨𝑥, 𝑦⟩})
5		vex 3475	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
6		vex 3475	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
7	5, 6	op2nda 6232	. . . . . . . . . 10 ⊢ ∪ ran {⟨𝑥, 𝑦⟩} = 𝑦
8	4, 7	eqtr2di 2785	. . . . . . . . 9 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ∪ ran {𝐴})
9	8	pm4.71ri 560	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
10	9	anbi1i 623	. . . . . . 7 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
11		anass 468	. . . . . . 7 ⊢ (((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
12	10, 11	bitri 275	. . . . . 6 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
13	12	exbii 1843	. . . . 5 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
14		snex 5433	. . . . . . . 8 ⊢ {𝐴} ∈ V
15	14	rnex 7918	. . . . . . 7 ⊢ ran {𝐴} ∈ V
16	15	uniex 7746	. . . . . 6 ⊢ ∪ ran {𝐴} ∈ V
17		opeq2 4875	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∪ ran {𝐴}⟩)
18	17	eqeq2d 2739	. . . . . . 7 ⊢ (𝑦 = ∪ ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
19		eleq1 2817	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → (𝑦 ∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶))
20	19	anbi2d 629	. . . . . . 7 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
21	18, 20	anbi12d 631	. . . . . 6 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
22	16, 21	ceqsexv 3523	. . . . 5 ⊢ (∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
23	13, 22	bitri 275	. . . 4 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
24		inteq 4952	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∩ 𝐴 = ∩ ⟨𝑥, ∪ ran {𝐴}⟩)
25	24	inteqd 4954	. . . . . . 7 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∩ ∩ 𝐴 = ∩ ∩ ⟨𝑥, ∪ ran {𝐴}⟩)
26	5, 16	op1stb 5473	. . . . . . 7 ⊢ ∩ ∩ ⟨𝑥, ∪ ran {𝐴}⟩ = 𝑥
27	25, 26	eqtr2di 2785	. . . . . 6 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → 𝑥 = ∩ ∩ 𝐴)
28	27	pm4.71ri 560	. . . . 5 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ (𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
29	28	anbi1i 623	. . . 4 ⊢ ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
30		anass 468	. . . 4 ⊢ (((𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
31	23, 29, 30	3bitri 297	. . 3 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
32	31	exbii 1843	. 2 ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
33		eqvisset 3489	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → ∩ ∩ 𝐴 ∈ V)
34	33	adantr 480	. . . 4 ⊢ ((𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V)
35	34	exlimiv 1926	. . 3 ⊢ (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V)
36		elex 3490	. . . 4 ⊢ (∩ ∩ 𝐴 ∈ 𝐵 → ∩ ∩ 𝐴 ∈ V)
37	36	ad2antrl 727	. . 3 ⊢ ((𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) → ∩ ∩ 𝐴 ∈ V)
38		opeq1 4874	. . . . . 6 ⊢ (𝑥 = ∩ ∩ 𝐴 → ⟨𝑥, ∪ ran {𝐴}⟩ = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩)
39	38	eqeq2d 2739	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ 𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩))
40		eleq1 2817	. . . . . 6 ⊢ (𝑥 = ∩ ∩ 𝐴 → (𝑥 ∈ 𝐵 ↔ ∩ ∩ 𝐴 ∈ 𝐵))
41	40	anbi1d 630	. . . . 5 ⊢ (𝑥 = ∩ ∩ 𝐴 → ((𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶) ↔ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
42	39, 41	anbi12d 631	. . . 4 ⊢ (𝑥 = ∩ ∩ 𝐴 → ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
43	42	ceqsexgv 3640	. . 3 ⊢ (∩ ∩ 𝐴 ∈ V → (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
44	35, 37, 43	pm5.21nii 378	. 2 ⊢ (∃𝑥(𝑥 = ∩ ∩ 𝐴 ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
45	1, 32, 44	3bitri 297	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1534  ∃wex 1774   ∈ wcel 2099  Vcvv 3471  {csn 4629  ⟨cop 4635  ∪ cuni 4908  ∩ cint 4949   × cxp 5676  ran crn 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429  ax-un 7740

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-br 5149  df-opab 5211  df-xp 5684  df-rel 5685  df-cnv 5686  df-dm 5688  df-rn 5689

This theorem is referenced by: (None)