Theorem elxp4 4828

Description: Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 4829. (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 2610	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 ∈ V)
2		elex 2610	. . . 4 ⊢ (∪ dom {𝐴} ∈ 𝐵 → ∪ dom {𝐴} ∈ V)
3		elex 2610	. . . 4 ⊢ (∪ ran {𝐴} ∈ 𝐶 → ∪ ran {𝐴} ∈ V)
4	2, 3	anim12i 331	. . 3 ⊢ ((∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶) → (∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V))
5		opexg 3983	. . . . 5 ⊢ ((∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V) → ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∈ V)
6	5	adantl 271	. . . 4 ⊢ ((𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V)) → ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∈ V)
7		eleq1 2141	. . . . 5 ⊢ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ → (𝐴 ∈ V ↔ ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∈ V))
8	7	adantr 270	. . . 4 ⊢ ((𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V)) → (𝐴 ∈ V ↔ ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∈ V))
9	6, 8	mpbird 165	. . 3 ⊢ ((𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ V ∧ ∪ ran {𝐴} ∈ V)) → 𝐴 ∈ V)
10	4, 9	sylan2 280	. 2 ⊢ ((𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) → 𝐴 ∈ V)
11		elxp 4380	. . . 4 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
12	11	a1i 9	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
13		sneq 3409	. . . . . . . . . . . . 13 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
14	13	rneqd 4581	. . . . . . . . . . . 12 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
15	14	unieqd 3612	. . . . . . . . . . 11 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ∪ ran {𝐴} = ∪ ran {⟨𝑥, 𝑦⟩})
16		vex 2604	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
17		vex 2604	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
18	16, 17	op2nda 4825	. . . . . . . . . . 11 ⊢ ∪ ran {⟨𝑥, 𝑦⟩} = 𝑦
19	15, 18	syl6req 2130	. . . . . . . . . 10 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ∪ ran {𝐴})
20	19	pm4.71ri 384	. . . . . . . . 9 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
21	20	anbi1i 445	. . . . . . . 8 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
22		anass 393	. . . . . . . 8 ⊢ (((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
23	21, 22	bitri 182	. . . . . . 7 ⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
24	23	exbii 1536	. . . . . 6 ⊢ (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
25		snexg 3956	. . . . . . . . 9 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
26		rnexg 4615	. . . . . . . . 9 ⊢ ({𝐴} ∈ V → ran {𝐴} ∈ V)
27	25, 26	syl 14	. . . . . . . 8 ⊢ (𝐴 ∈ V → ran {𝐴} ∈ V)
28		uniexg 4193	. . . . . . . 8 ⊢ (ran {𝐴} ∈ V → ∪ ran {𝐴} ∈ V)
29	27, 28	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ V → ∪ ran {𝐴} ∈ V)
30		opeq2 3571	. . . . . . . . . 10 ⊢ (𝑦 = ∪ ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∪ ran {𝐴}⟩)
31	30	eqeq2d 2092	. . . . . . . . 9 ⊢ (𝑦 = ∪ ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩))
32		eleq1 2141	. . . . . . . . . 10 ⊢ (𝑦 = ∪ ran {𝐴} → (𝑦 ∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶))
33	32	anbi2d 451	. . . . . . . . 9 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
34	31, 33	anbi12d 456	. . . . . . . 8 ⊢ (𝑦 = ∪ ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
35	34	ceqsexgv 2724	. . . . . . 7 ⊢ (∪ ran {𝐴} ∈ V → (∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
36	29, 35	syl 14	. . . . . 6 ⊢ (𝐴 ∈ V → (∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
37	24, 36	syl5bb 190	. . . . 5 ⊢ (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
38		sneq 3409	. . . . . . . . . . . 12 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → {𝐴} = {⟨𝑥, ∪ ran {𝐴}⟩})
39	38	dmeqd 4555	. . . . . . . . . . 11 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ∪ ran {𝐴}⟩})
40	39	unieqd 3612	. . . . . . . . . 10 ⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∪ dom {𝐴} = ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩})
41	40	adantl 271	. . . . . . . . 9 ⊢ ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) → ∪ dom {𝐴} = ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩})
42		dmsnopg 4812	. . . . . . . . . . . . 13 ⊢ (∪ ran {𝐴} ∈ V → dom {⟨𝑥, ∪ ran {𝐴}⟩} = {𝑥})
43	29, 42	syl 14	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V → dom {⟨𝑥, ∪ ran {𝐴}⟩} = {𝑥})
44	43	unieqd 3612	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩} = ∪ {𝑥})
45	16	unisn 3617	. . . . . . . . . . 11 ⊢ ∪ {𝑥} = 𝑥
46	44, 45	syl6eq 2129	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩} = 𝑥)
47	46	adantr 270	. . . . . . . . 9 ⊢ ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) → ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩} = 𝑥)
48	41, 47	eqtr2d 2114	. . . . . . . 8 ⊢ ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) → 𝑥 = ∪ dom {𝐴})
49	48	ex 113	. . . . . . 7 ⊢ (𝐴 ∈ V → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → 𝑥 = ∪ dom {𝐴}))
50	49	pm4.71rd 386	. . . . . 6 ⊢ (𝐴 ∈ V → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ (𝑥 = ∪ dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩)))
51	50	anbi1d 452	. . . . 5 ⊢ (𝐴 ∈ V → ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = ∪ dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
52		anass 393	. . . . . 6 ⊢ (((𝑥 = ∪ dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
53	52	a1i 9	. . . . 5 ⊢ (𝐴 ∈ V → (((𝑥 = ∪ dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))))
54	37, 51, 53	3bitrd 212	. . . 4 ⊢ (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))))
55	54	exbidv 1746	. . 3 ⊢ (𝐴 ∈ V → (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥(𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))))
56		dmexg 4614	. . . . . 6 ⊢ ({𝐴} ∈ V → dom {𝐴} ∈ V)
57	25, 56	syl 14	. . . . 5 ⊢ (𝐴 ∈ V → dom {𝐴} ∈ V)
58		uniexg 4193	. . . . 5 ⊢ (dom {𝐴} ∈ V → ∪ dom {𝐴} ∈ V)
59	57, 58	syl 14	. . . 4 ⊢ (𝐴 ∈ V → ∪ dom {𝐴} ∈ V)
60		opeq1 3570	. . . . . . 7 ⊢ (𝑥 = ∪ dom {𝐴} → ⟨𝑥, ∪ ran {𝐴}⟩ = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩)
61	60	eqeq2d 2092	. . . . . 6 ⊢ (𝑥 = ∪ dom {𝐴} → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ 𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩))
62		eleq1 2141	. . . . . . 7 ⊢ (𝑥 = ∪ dom {𝐴} → (𝑥 ∈ 𝐵 ↔ ∪ dom {𝐴} ∈ 𝐵))
63	62	anbi1d 452	. . . . . 6 ⊢ (𝑥 = ∪ dom {𝐴} → ((𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶) ↔ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
64	61, 63	anbi12d 456	. . . . 5 ⊢ (𝑥 = ∪ dom {𝐴} → ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
65	64	ceqsexgv 2724	. . . 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 212	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))))
68	1, 10, 67	pm5.21nii 652	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))

Syntax hints:   ∧ wa 102   ↔ wb 103   = wceq 1284  ∃wex 1421   ∈ wcel 1433  Vcvv 2601  {csn 3398  ⟨cop 3401  ∪ cuni 3601   × cxp 4361  dom cdm 4363  ran crn 4364

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964  ax-un 4188

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-opab 3840  df-xp 4369  df-rel 4370  df-cnv 4371  df-dm 4373  df-rn 4374

This theorem is referenced by:  elxp6  5816  xpdom2  6328