Theorem elxp4 5224

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

Assertion

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

Proof of Theorem elxp4

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

Step	Hyp	Ref	Expression
1		elex 2814	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 ∈ V)
2		elex 2814	. . . 4 ⊢ (∪ dom {𝐴} ∈ 𝐵 → ∪ dom {𝐴} ∈ V)
3		elex 2814	. . . 4 ⊢ (∪ ran {𝐴} ∈ 𝐶 → ∪ ran {𝐴} ∈ V)
4	2, 3	anim12i 338	. . 3 ⊢ ((∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶) → (∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V))
5		opexg 4320	. . . . 5 ⊢ ((∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V) → ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∈ V)
6	5	adantl 277	. . . 4 ⊢ ((𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V)) → ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∈ V)
7		eleq1 2294	. . . . 5 ⊢ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ → (𝐴 ∈ V ↔ ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∈ V))
8	7	adantr 276	. . . 4 ⊢ ((𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V)) → (𝐴 ∈ V ↔ ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∈ V))
9	6, 8	mpbird 167	. . 3 ⊢ ((𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V)) → 𝐴 ∈ V)
10	4, 9	sylan2 286	. 2 ⊢ ((𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) → 𝐴 ∈ V)
11		elxp 4742	. . . 4 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
12	11	a1i 9	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
13		sneq 3680	. . . . . . . . . . . . 13 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
14	13	rneqd 4961	. . . . . . . . . . . 12 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
15	14	unieqd 3904	. . . . . . . . . . 11 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ∪ ran {𝐴} = ∪ ran {⟨𝑥, 𝑦⟩})
16		vex 2805	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
17		vex 2805	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
18	16, 17	op2nda 5221	. . . . . . . . . . 11 ⊢ ∪ ran {⟨𝑥, 𝑦⟩} = 𝑦
19	15, 18	eqtr2di 2281	. . . . . . . . . 10 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ∪ ran {𝐴})
20	19	pm4.71ri 392	. . . . . . . . 9 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
21	20	anbi1i 458	. . . . . . . 8 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
22		anass 401	. . . . . . . 8 ⊢ (((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
23	21, 22	bitri 184	. . . . . . 7 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
24	23	exbii 1653	. . . . . 6 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
25		snexg 4274	. . . . . . . . 9 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
26		rnexg 4997	. . . . . . . . 9 ⊢ ({𝐴} ∈ V → ran {𝐴} ∈ V)
27	25, 26	syl 14	. . . . . . . 8 ⊢ (𝐴 ∈ V → ran {𝐴} ∈ V)
28		uniexg 4536	. . . . . . . 8 ⊢ (ran {𝐴} ∈ V → ∪ ran {𝐴} ∈ V)
29	27, 28	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ V → ∪ ran {𝐴} ∈ V)
30		opeq2 3863	. . . . . . . . . 10 ⊢ (𝑦 = ∪ ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∪ ran {𝐴}⟩)
31	30	eqeq2d 2243	. . . . . . . . 9 ⊢ (𝑦 = ∪ ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
32		eleq1 2294	. . . . . . . . . 10 ⊢ (𝑦 = ∪ ran {𝐴} → (𝑦 ∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶))
33	32	anbi2d 464	. . . . . . . . 9 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
34	31, 33	anbi12d 473	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
35	34	ceqsexgv 2935	. . . . . . 7 ⊢ (∪ ran {𝐴} ∈ V → (∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
36	29, 35	syl 14	. . . . . 6 ⊢ (𝐴 ∈ V → (∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
37	24, 36	bitrid 192	. . . . 5 ⊢ (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
38		sneq 3680	. . . . . . . . . . . 12 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → {𝐴} = {⟨𝑥, ∪ ran {𝐴}⟩})
39	38	dmeqd 4933	. . . . . . . . . . 11 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ∪ ran {𝐴}⟩})
40	39	unieqd 3904	. . . . . . . . . 10 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∪ dom {𝐴} = ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩})
41	40	adantl 277	. . . . . . . . 9 ⊢ ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) → ∪ dom {𝐴} = ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩})
42		dmsnopg 5208	. . . . . . . . . . . . 13 ⊢ (∪ ran {𝐴} ∈ V → dom {⟨𝑥, ∪ ran {𝐴}⟩} = {𝑥})
43	29, 42	syl 14	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V → dom {⟨𝑥, ∪ ran {𝐴}⟩} = {𝑥})
44	43	unieqd 3904	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩} = ∪ {𝑥})
45	16	unisn 3909	. . . . . . . . . . 11 ⊢ ∪ {𝑥} = 𝑥
46	44, 45	eqtrdi 2280	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩} = 𝑥)
47	46	adantr 276	. . . . . . . . 9 ⊢ ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) → ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩} = 𝑥)
48	41, 47	eqtr2d 2265	. . . . . . . 8 ⊢ ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) → 𝑥 = ∪ dom {𝐴})
49	48	ex 115	. . . . . . 7 ⊢ (𝐴 ∈ V → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → 𝑥 = ∪ dom {𝐴}))
50	49	pm4.71rd 394	. . . . . 6 ⊢ (𝐴 ∈ V → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ (𝑥 = ∪ dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩)))
51	50	anbi1d 465	. . . . 5 ⊢ (𝐴 ∈ V → ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = ∪ dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
52		anass 401	. . . . . 6 ⊢ (((𝑥 = ∪ dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
53	52	a1i 9	. . . . 5 ⊢ (𝐴 ∈ V → (((𝑥 = ∪ dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))))
54	37, 51, 53	3bitrd 214	. . . 4 ⊢ (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))))
55	54	exbidv 1873	. . 3 ⊢ (𝐴 ∈ V → (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥(𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))))
56		dmexg 4996	. . . . . 6 ⊢ ({𝐴} ∈ V → dom {𝐴} ∈ V)
57	25, 56	syl 14	. . . . 5 ⊢ (𝐴 ∈ V → dom {𝐴} ∈ V)
58		uniexg 4536	. . . . 5 ⊢ (dom {𝐴} ∈ V → ∪ dom {𝐴} ∈ V)
59	57, 58	syl 14	. . . 4 ⊢ (𝐴 ∈ V → ∪ dom {𝐴} ∈ V)
60		opeq1 3862	. . . . . . 7 ⊢ (𝑥 = ∪ dom {𝐴} → ⟨𝑥, ∪ ran {𝐴}⟩ = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩)
61	60	eqeq2d 2243	. . . . . 6 ⊢ (𝑥 = ∪ dom {𝐴} → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ 𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩))
62		eleq1 2294	. . . . . . 7 ⊢ (𝑥 = ∪ dom {𝐴} → (𝑥 ∈ 𝐵 ↔ ∪ dom {𝐴} ∈ 𝐵))
63	62	anbi1d 465	. . . . . 6 ⊢ (𝑥 = ∪ dom {𝐴} → ((𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶) ↔ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
64	61, 63	anbi12d 473	. . . . 5 ⊢ (𝑥 = ∪ dom {𝐴} → ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
65	64	ceqsexgv 2935	. . . 4 ⊢ (∪ dom {𝐴} ∈ V → (∃𝑥(𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
66	59, 65	syl 14	. . 3 ⊢ (𝐴 ∈ V → (∃𝑥(𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
67	12, 55, 66	3bitrd 214	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
68	1, 10, 67	pm5.21nii 711	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1397  ∃wex 1540   ∈ wcel 2202  Vcvv 2802  {csn 3669  ⟨cop 3672  ∪ cuni 3893   × cxp 4723  dom cdm 4725  ran crn 4726

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-xp 4731  df-rel 4732  df-cnv 4733  df-dm 4735  df-rn 4736

This theorem is referenced by:  elxp6  6331  xpdom2  7014