Theorem elxp5 4752

Description: Membership in a cross product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 4751 when the double intersection does not create class existence problems (caused by int0 3620). (Contributed by NM, 1-Aug-2004.)

Assertion

Ref	Expression
elxp5	|- (A e. (B X. C) <-> (A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. B /\ U. ran {A } e. C)))

Proof of Theorem elxp5

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

Step	Hyp	Ref	Expression
1		elex 2560	. 2 |- (A e. (B X. C) -> A e. _V)
2		elex 2560	. . . 4 |- ( |^| |^|A e. B -> |^| |^|A e. _V)
3		elex 2560	. . . 4 |- ( U. ran {A } e. C -> U. ran {A } e. _V)
4	2, 3	anim12i 321	. . 3 |- (( |^| |^|A e. B /\ U. ran {A } e. C) -> ( |^| |^|A e. _V /\ U. ran {A } e. _V))
5		opexgOLD 3956	. . . . 5 |- (( |^| |^|A e. _V /\ U. ran {A } e. _V) -> <. |^| |^|A , U. ran {A } >. e. _V)
6	5	adantl 262	. . . 4 |- ((A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. _V /\ U. ran {A } e. _V)) -> <. |^| |^|A , U. ran {A } >. e. _V)
7		eleq1 2097	. . . . 5 |- (A = <. |^| |^|A , U. ran {A } >. -> (A e. _V <-> <. |^| |^|A , U. ran {A } >. e. _V))
8	7	adantr 261	. . . 4 |- ((A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. _V /\ U. ran {A } e. _V)) -> (A e. _V <-> <. |^| |^|A , U. ran {A } >. e. _V))
9	6, 8	mpbird 156	. . 3 |- ((A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. _V /\ U. ran {A } e. _V)) -> A e. _V)
10	4, 9	sylan2 270	. 2 |- ((A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. B /\ U. ran {A } e. C)) -> A e. _V)
11		elxp 4305	. . . 4 |- (A e. (B X. C) <-> E.xE.y(A = <.x , y >. /\ (x e. B /\ y e. C)))
12		sneq 3378	. . . . . . . . . . . . . 14 |- (A = <.x , y >. -> {A } = { <.x , y >. })
13	12	rneqd 4506	. . . . . . . . . . . . 13 |- (A = <.x , y >. -> ran {A } = ran { <.x , y >. })
14	13	unieqd 3582	. . . . . . . . . . . 12 |- (A = <.x , y >. -> U. ran {A } = U. ran { <.x , y >. })
15		vex 2554	. . . . . . . . . . . . 13 |- x e. _V
16		vex 2554	. . . . . . . . . . . . 13 |- y e. _V
17	15, 16	op2nda 4748	. . . . . . . . . . . 12 |- U. ran { <.x , y >. } = y
18	14, 17	syl6req 2086	. . . . . . . . . . 11 |- (A = <.x , y >. -> y = U. ran {A })
19	18	pm4.71ri 372	. . . . . . . . . 10 |- (A = <.x , y >. <-> (y = U. ran {A } /\ A = <.x , y >.))
20	19	anbi1i 431	. . . . . . . . 9 |- ((A = <.x , y >. /\ (x e. B /\ y e. C)) <-> ((y = U. ran {A } /\ A = <.x , y >.) /\ (x e. B /\ y e. C)))
21		anass 381	. . . . . . . . 9 |- (((y = U. ran {A } /\ A = <.x , y >.) /\ (x e. B /\ y e. C)) <-> (y = U. ran {A } /\ (A = <.x , y >. /\ (x e. B /\ y e. C))))
22	20, 21	bitri 173	. . . . . . . 8 |- ((A = <.x , y >. /\ (x e. B /\ y e. C)) <-> (y = U. ran {A } /\ (A = <.x , y >. /\ (x e. B /\ y e. C))))
23	22	exbii 1493	. . . . . . 7 |- (E.y(A = <.x , y >. /\ (x e. B /\ y e. C)) <-> E.y(y = U. ran {A } /\ (A = <.x , y >. /\ (x e. B /\ y e. C))))
24		snexgOLD 3926	. . . . . . . . . 10 |- (A e. _V -> {A } e. _V)
25		rnexg 4540	. . . . . . . . . 10 |- ( {A } e. _V -> ran {A } e. _V)
26	24, 25	syl 14	. . . . . . . . 9 |- (A e. _V -> ran {A } e. _V)
27		uniexg 4141	. . . . . . . . 9 |- ( ran {A } e. _V -> U. ran {A } e. _V)
28	26, 27	syl 14	. . . . . . . 8 |- (A e. _V -> U. ran {A } e. _V)
29		opeq2 3541	. . . . . . . . . . 11 |- (y = U. ran {A } -> <.x , y >. = <.x , U. ran {A } >.)
30	29	eqeq2d 2048	. . . . . . . . . 10 |- (y = U. ran {A } -> (A = <.x , y >. <-> A = <.x , U. ran {A } >.))
31		eleq1 2097	. . . . . . . . . . 11 |- (y = U. ran {A } -> (y e. C <-> U. ran {A } e. C))
32	31	anbi2d 437	. . . . . . . . . 10 |- (y = U. ran {A } -> ((x e. B /\ y e. C) <-> (x e. B /\ U. ran {A } e. C)))
33	30, 32	anbi12d 442	. . . . . . . . 9 |- (y = U. ran {A } -> ((A = <.x , y >. /\ (x e. B /\ y e. C)) <-> (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C))))
34	33	ceqsexgv 2667	. . . . . . . 8 |- ( U. ran {A } e. _V -> (E.y(y = U. ran {A } /\ (A = <.x , y >. /\ (x e. B /\ y e. C))) <-> (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C))))
35	28, 34	syl 14	. . . . . . 7 |- (A e. _V -> (E.y(y = U. ran {A } /\ (A = <.x , y >. /\ (x e. B /\ y e. C))) <-> (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C))))
36	23, 35	syl5bb 181	. . . . . 6 |- (A e. _V -> (E.y(A = <.x , y >. /\ (x e. B /\ y e. C)) <-> (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C))))
37		inteq 3609	. . . . . . . . . . . 12 |- (A = <.x , U. ran {A } >. -> |^|A = |^| <.x , U. ran {A } >.)
38	37	inteqd 3611	. . . . . . . . . . 11 |- (A = <.x , U. ran {A } >. -> |^| |^|A = |^| |^| <.x , U. ran {A } >.)
39	38	adantl 262	. . . . . . . . . 10 |- ((A e. _V /\ A = <.x , U. ran {A } >.) -> |^| |^|A = |^| |^| <.x , U. ran {A } >.)
40		op1stbg 4176	. . . . . . . . . . . 12 |- ((x e. _V /\ U. ran {A } e. _V) -> |^| |^| <.x , U. ran {A } >. = x)
41	15, 28, 40	sylancr 393	. . . . . . . . . . 11 |- (A e. _V -> |^| |^| <.x , U. ran {A } >. = x)
42	41	adantr 261	. . . . . . . . . 10 |- ((A e. _V /\ A = <.x , U. ran {A } >.) -> |^| |^| <.x , U. ran {A } >. = x)
43	39, 42	eqtr2d 2070	. . . . . . . . 9 |- ((A e. _V /\ A = <.x , U. ran {A } >.) -> x = |^| |^|A)
44	43	ex 108	. . . . . . . 8 |- (A e. _V -> (A = <.x , U. ran {A } >. -> x = |^| |^|A))
45	44	pm4.71rd 374	. . . . . . 7 |- (A e. _V -> (A = <.x , U. ran {A } >. <-> (x = |^| |^|A /\ A = <.x , U. ran {A } >.)))
46	45	anbi1d 438	. . . . . 6 |- (A e. _V -> ((A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C)) <-> ((x = |^| |^|A /\ A = <.x , U. ran {A } >.) /\ (x e. B /\ U. ran {A } e. C))))
47		anass 381	. . . . . . 7 |- (((x = |^| |^|A /\ A = <.x , U. ran {A } >.) /\ (x e. B /\ U. ran {A } e. C)) <-> (x = |^| |^|A /\ (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C))))
48	47	a1i 9	. . . . . 6 |- (A e. _V -> (((x = |^| |^|A /\ A = <.x , U. ran {A } >.) /\ (x e. B /\ U. ran {A } e. C)) <-> (x = |^| |^|A /\ (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C)))))
49	36, 46, 48	3bitrd 203	. . . . 5 |- (A e. _V -> (E.y(A = <.x , y >. /\ (x e. B /\ y e. C)) <-> (x = |^| |^|A /\ (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C)))))
50	49	exbidv 1703	. . . 4 |- (A e. _V -> (E.xE.y(A = <.x , y >. /\ (x e. B /\ y e. C)) <-> E.x(x = |^| |^|A /\ (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C)))))
51	11, 50	syl5bb 181	. . 3 |- (A e. _V -> (A e. (B X. C) <-> E.x(x = |^| |^|A /\ (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C)))))
52		eleq1 2097	. . . . . . 7 |- (x = |^| |^|A -> (x e. _V <-> |^| |^|A e. _V))
53	15, 52	mpbii 136	. . . . . 6 |- (x = |^| |^|A -> |^| |^|A e. _V)
54	53	adantr 261	. . . . 5 |- ((x = |^| |^|A /\ (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C))) -> |^| |^|A e. _V)
55	54	exlimiv 1486	. . . 4 |- (E.x(x = |^| |^|A /\ (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C))) -> |^| |^|A e. _V)
56	2	ad2antrl 459	. . . 4 |- ((A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. B /\ U. ran {A } e. C)) -> |^| |^|A e. _V)
57		opeq1 3540	. . . . . . 7 |- (x = |^| |^|A -> <.x , U. ran {A } >. = <. |^| |^|A , U. ran {A } >.)
58	57	eqeq2d 2048	. . . . . 6 |- (x = |^| |^|A -> (A = <.x , U. ran {A } >. <-> A = <. |^| |^|A , U. ran {A } >.))
59		eleq1 2097	. . . . . . 7 |- (x = |^| |^|A -> (x e. B <-> |^| |^|A e. B))
60	59	anbi1d 438	. . . . . 6 |- (x = |^| |^|A -> ((x e. B /\ U. ran {A } e. C) <-> ( |^| |^|A e. B /\ U. ran {A } e. C)))
61	58, 60	anbi12d 442	. . . . 5 |- (x = |^| |^|A -> ((A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C)) <-> (A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. B /\ U. ran {A } e. C))))
62	61	ceqsexgv 2667	. . . 4 |- ( |^| |^|A e. _V -> (E.x(x = |^| |^|A /\ (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C))) <-> (A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. B /\ U. ran {A } e. C))))
63	55, 56, 62	pm5.21nii 619	. . 3 |- (E.x(x = |^| |^|A /\ (A = <.x , U. ran {A } >. /\ (x e. B /\ U. ran {A } e. C))) <-> (A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. B /\ U. ran {A } e. C)))
64	51, 63	syl6bb 185	. 2 |- (A e. _V -> (A e. (B X. C) <-> (A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. B /\ U. ran {A } e. C))))
65	1, 10, 64	pm5.21nii 619	1 |- (A e. (B X. C) <-> (A = <. |^| |^|A , U. ran {A } >. /\ ( |^| |^|A e. B /\ U. ran {A } e. C)))

Syntax hints:   /\ wa 97   <-> wb 98   = wceq 1242  E.wex 1378   e. wcel 1390   _Vcvv 2551   {csn 3367   <.cop 3370   U.cuni 3571   |^|cint 3606   X. cxp 4286   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-bnd 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-int 3607  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: (None)