Theorem elxp4 4751

Description: Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 4752. (Contributed by NM, 17-Feb-2004.)

Assertion

Ref	Expression
elxp4	⊢ (A ∈ (B × 𝐶) ↔ (A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶)))

Proof of Theorem elxp4

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

Step	Hyp	Ref	Expression
1		elex 2560	. 2 ⊢ (A ∈ (B × 𝐶) → A ∈ V)
2		elex 2560	. . . 4 ⊢ (∪ dom {A} ∈ B → ∪ dom {A} ∈ V)
3		elex 2560	. . . 4 ⊢ (∪ ran {A} ∈ 𝐶 → ∪ ran {A} ∈ V)
4	2, 3	anim12i 321	. . 3 ⊢ ((∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶) → (∪ dom {A} ∈ V ∧ ∪ ran {A} ∈ V))
5		opexgOLD 3956	. . . . 5 ⊢ ((∪ dom {A} ∈ V ∧ ∪ ran {A} ∈ V) → ⟨∪ dom {A}, ∪ ran {A}⟩ ∈ V)
6	5	adantl 262	. . . 4 ⊢ ((A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ V ∧ ∪ ran {A} ∈ V)) → ⟨∪ dom {A}, ∪ ran {A}⟩ ∈ V)
7		eleq1 2097	. . . . 5 ⊢ (A = ⟨∪ dom {A}, ∪ ran {A}⟩ → (A ∈ V ↔ ⟨∪ dom {A}, ∪ ran {A}⟩ ∈ V))
8	7	adantr 261	. . . 4 ⊢ ((A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ V ∧ ∪ ran {A} ∈ V)) → (A ∈ V ↔ ⟨∪ dom {A}, ∪ ran {A}⟩ ∈ V))
9	6, 8	mpbird 156	. . 3 ⊢ ((A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ V ∧ ∪ ran {A} ∈ V)) → A ∈ V)
10	4, 9	sylan2 270	. 2 ⊢ ((A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶)) → A ∈ V)
11		elxp 4305	. . . 4 ⊢ (A ∈ (B × 𝐶) ↔ ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)))
12	11	a1i 9	. . 3 ⊢ (A ∈ V → (A ∈ (B × 𝐶) ↔ ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶))))
13		sneq 3378	. . . . . . . . . . . . 13 ⊢ (A = ⟨x, y⟩ → {A} = {⟨x, y⟩})
14	13	rneqd 4506	. . . . . . . . . . . 12 ⊢ (A = ⟨x, y⟩ → ran {A} = ran {⟨x, y⟩})
15	14	unieqd 3582	. . . . . . . . . . 11 ⊢ (A = ⟨x, y⟩ → ∪ ran {A} = ∪ ran {⟨x, y⟩})
16		vex 2554	. . . . . . . . . . . 12 ⊢ x ∈ V
17		vex 2554	. . . . . . . . . . . 12 ⊢ y ∈ V
18	16, 17	op2nda 4748	. . . . . . . . . . 11 ⊢ ∪ ran {⟨x, y⟩} = y
19	15, 18	syl6req 2086	. . . . . . . . . 10 ⊢ (A = ⟨x, y⟩ → y = ∪ ran {A})
20	19	pm4.71ri 372	. . . . . . . . 9 ⊢ (A = ⟨x, y⟩ ↔ (y = ∪ ran {A} ∧ A = ⟨x, y⟩))
21	20	anbi1i 431	. . . . . . . 8 ⊢ ((A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)) ↔ ((y = ∪ ran {A} ∧ A = ⟨x, y⟩) ∧ (x ∈ B ∧ y ∈ 𝐶)))
22		anass 381	. . . . . . . 8 ⊢ (((y = ∪ ran {A} ∧ A = ⟨x, y⟩) ∧ (x ∈ B ∧ y ∈ 𝐶)) ↔ (y = ∪ ran {A} ∧ (A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶))))
23	21, 22	bitri 173	. . . . . . 7 ⊢ ((A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)) ↔ (y = ∪ ran {A} ∧ (A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶))))
24	23	exbii 1493	. . . . . 6 ⊢ (∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)) ↔ ∃y(y = ∪ ran {A} ∧ (A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶))))
25		snexgOLD 3926	. . . . . . . . 9 ⊢ (A ∈ V → {A} ∈ V)
26		rnexg 4540	. . . . . . . . 9 ⊢ ({A} ∈ V → ran {A} ∈ V)
27	25, 26	syl 14	. . . . . . . 8 ⊢ (A ∈ V → ran {A} ∈ V)
28		uniexg 4141	. . . . . . . 8 ⊢ (ran {A} ∈ V → ∪ ran {A} ∈ V)
29	27, 28	syl 14	. . . . . . 7 ⊢ (A ∈ V → ∪ ran {A} ∈ V)
30		opeq2 3541	. . . . . . . . . 10 ⊢ (y = ∪ ran {A} → ⟨x, y⟩ = ⟨x, ∪ ran {A}⟩)
31	30	eqeq2d 2048	. . . . . . . . 9 ⊢ (y = ∪ ran {A} → (A = ⟨x, y⟩ ↔ A = ⟨x, ∪ ran {A}⟩))
32		eleq1 2097	. . . . . . . . . 10 ⊢ (y = ∪ ran {A} → (y ∈ 𝐶 ↔ ∪ ran {A} ∈ 𝐶))
33	32	anbi2d 437	. . . . . . . . 9 ⊢ (y = ∪ ran {A} → ((x ∈ B ∧ y ∈ 𝐶) ↔ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶)))
34	31, 33	anbi12d 442	. . . . . . . 8 ⊢ (y = ∪ ran {A} → ((A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)) ↔ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
35	34	ceqsexgv 2667	. . . . . . 7 ⊢ (∪ ran {A} ∈ V → (∃y(y = ∪ ran {A} ∧ (A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶))) ↔ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
36	29, 35	syl 14	. . . . . 6 ⊢ (A ∈ V → (∃y(y = ∪ ran {A} ∧ (A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶))) ↔ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
37	24, 36	syl5bb 181	. . . . 5 ⊢ (A ∈ V → (∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)) ↔ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
38		sneq 3378	. . . . . . . . . . . 12 ⊢ (A = ⟨x, ∪ ran {A}⟩ → {A} = {⟨x, ∪ ran {A}⟩})
39	38	dmeqd 4480	. . . . . . . . . . 11 ⊢ (A = ⟨x, ∪ ran {A}⟩ → dom {A} = dom {⟨x, ∪ ran {A}⟩})
40	39	unieqd 3582	. . . . . . . . . 10 ⊢ (A = ⟨x, ∪ ran {A}⟩ → ∪ dom {A} = ∪ dom {⟨x, ∪ ran {A}⟩})
41	40	adantl 262	. . . . . . . . 9 ⊢ ((A ∈ V ∧ A = ⟨x, ∪ ran {A}⟩) → ∪ dom {A} = ∪ dom {⟨x, ∪ ran {A}⟩})
42		dmsnopg 4735	. . . . . . . . . . . . 13 ⊢ (∪ ran {A} ∈ V → dom {⟨x, ∪ ran {A}⟩} = {x})
43	29, 42	syl 14	. . . . . . . . . . . 12 ⊢ (A ∈ V → dom {⟨x, ∪ ran {A}⟩} = {x})
44	43	unieqd 3582	. . . . . . . . . . 11 ⊢ (A ∈ V → ∪ dom {⟨x, ∪ ran {A}⟩} = ∪ {x})
45	16	unisn 3587	. . . . . . . . . . 11 ⊢ ∪ {x} = x
46	44, 45	syl6eq 2085	. . . . . . . . . 10 ⊢ (A ∈ V → ∪ dom {⟨x, ∪ ran {A}⟩} = x)
47	46	adantr 261	. . . . . . . . 9 ⊢ ((A ∈ V ∧ A = ⟨x, ∪ ran {A}⟩) → ∪ dom {⟨x, ∪ ran {A}⟩} = x)
48	41, 47	eqtr2d 2070	. . . . . . . 8 ⊢ ((A ∈ V ∧ A = ⟨x, ∪ ran {A}⟩) → x = ∪ dom {A})
49	48	ex 108	. . . . . . 7 ⊢ (A ∈ V → (A = ⟨x, ∪ ran {A}⟩ → x = ∪ dom {A}))
50	49	pm4.71rd 374	. . . . . 6 ⊢ (A ∈ V → (A = ⟨x, ∪ ran {A}⟩ ↔ (x = ∪ dom {A} ∧ A = ⟨x, ∪ ran {A}⟩)))
51	50	anbi1d 438	. . . . 5 ⊢ (A ∈ V → ((A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶)) ↔ ((x = ∪ dom {A} ∧ A = ⟨x, ∪ ran {A}⟩) ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
52		anass 381	. . . . . 6 ⊢ (((x = ∪ dom {A} ∧ A = ⟨x, ∪ ran {A}⟩) ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶)) ↔ (x = ∪ dom {A} ∧ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
53	52	a1i 9	. . . . 5 ⊢ (A ∈ V → (((x = ∪ dom {A} ∧ A = ⟨x, ∪ ran {A}⟩) ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶)) ↔ (x = ∪ dom {A} ∧ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶)))))
54	37, 51, 53	3bitrd 203	. . . 4 ⊢ (A ∈ V → (∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)) ↔ (x = ∪ dom {A} ∧ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶)))))
55	54	exbidv 1703	. . 3 ⊢ (A ∈ V → (∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)) ↔ ∃x(x = ∪ dom {A} ∧ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶)))))
56		dmexg 4539	. . . . . 6 ⊢ ({A} ∈ V → dom {A} ∈ V)
57	25, 56	syl 14	. . . . 5 ⊢ (A ∈ V → dom {A} ∈ V)
58		uniexg 4141	. . . . 5 ⊢ (dom {A} ∈ V → ∪ dom {A} ∈ V)
59	57, 58	syl 14	. . . 4 ⊢ (A ∈ V → ∪ dom {A} ∈ V)
60		opeq1 3540	. . . . . . 7 ⊢ (x = ∪ dom {A} → ⟨x, ∪ ran {A}⟩ = ⟨∪ dom {A}, ∪ ran {A}⟩)
61	60	eqeq2d 2048	. . . . . 6 ⊢ (x = ∪ dom {A} → (A = ⟨x, ∪ ran {A}⟩ ↔ A = ⟨∪ dom {A}, ∪ ran {A}⟩))
62		eleq1 2097	. . . . . . 7 ⊢ (x = ∪ dom {A} → (x ∈ B ↔ ∪ dom {A} ∈ B))
63	62	anbi1d 438	. . . . . 6 ⊢ (x = ∪ dom {A} → ((x ∈ B ∧ ∪ ran {A} ∈ 𝐶) ↔ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶)))
64	61, 63	anbi12d 442	. . . . 5 ⊢ (x = ∪ dom {A} → ((A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶)) ↔ (A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
65	64	ceqsexgv 2667	. . . 4 ⊢ (∪ dom {A} ∈ V → (∃x(x = ∪ dom {A} ∧ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶))) ↔ (A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
66	59, 65	syl 14	. . 3 ⊢ (A ∈ V → (∃x(x = ∪ dom {A} ∧ (A = ⟨x, ∪ ran {A}⟩ ∧ (x ∈ B ∧ ∪ ran {A} ∈ 𝐶))) ↔ (A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
67	12, 55, 66	3bitrd 203	. 2 ⊢ (A ∈ V → (A ∈ (B × 𝐶) ↔ (A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶))))
68	1, 10, 67	pm5.21nii 619	1 ⊢ (A ∈ (B × 𝐶) ↔ (A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶)))

Syntax hints:   ∧ wa 97   ↔ wb 98   = wceq 1242  ∃wex 1378   ∈ wcel 1390  Vcvv 2551  {csn 3367  ⟨cop 3370  ∪ cuni 3571   × cxp 4286  dom cdm 4288  ran crn 4289

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-xp 4294  df-rel 4295  df-cnv 4296  df-dm 4298  df-rn 4299

This theorem is referenced by:  elxp6  5738  xpdom2  6241