Theorem ranncnt 15364

Description: Range of the intersection of the inclusion with a square cross product.

Hypothesis

Ref	Expression
ranncnt.1	|- C = {<.x, y>. | x C_ y}

Assertion

Ref	Expression
ranncnt	|- ran ( C i^i (A X. A)) = A

Distinct variable group:   x,A,y

Proof of Theorem ranncnt

Step	Hyp	Ref	Expression
1		ranncnt.1	. . . 4 |- C = {<.x, y>. | x C_ y}
2		df-xp 4133	. . . 4 |- (A X. A) = {<.x, y>. | (x e. A /\ y e. A)}
3	1, 2	ineq12i 3007	. . 3 |- (C i^i (A X. A)) = ({<.x, y>. | x C_ y} i^i {<.x, y>. | (x e. A /\ y e. A)})
4	3	rneqi 4308	. 2 |- ran ( C i^i (A X. A)) = ran ({<.x, y>. | x C_ y} i^i {<.x, y>. | (x e. A /\ y e. A)})
5		incom 3000	. . . 4 |- ({<.x, y>. | x C_ y} i^i {<.x, y>. | (x e. A /\ y e. A)}) = ({<.x, y>. | (x e. A /\ y e. A)} i^i {<.x, y>. | x C_ y})
6		inopab 4238	. . . 4 |- ({<.x, y>. | (x e. A /\ y e. A)} i^i {<.x, y>. | x C_ y}) = {<.x, y>. | ((x e. A /\ y e. A) /\ x C_ y)}
7	5, 6	eqtri 2161	. . 3 |- ({<.x, y>. | x C_ y} i^i {<.x, y>. | (x e. A /\ y e. A)}) = {<.x, y>. | ((x e. A /\ y e. A) /\ x C_ y)}
8	7	rneqi 4308	. 2 |- ran ({<.x, y>. | x C_ y} i^i {<.x, y>. | (x e. A /\ y e. A)}) = ran {<.x, y>. | ((x e. A /\ y e. A) /\ x C_ y)}
9		df-rn 4138	. . 3 |- ran {<.x, y>. | ((x e. A /\ y e. A) /\ x C_ y)} = dom `'{<.x, y>. | ((x e. A /\ y e. A) /\ x C_ y)}
10		cnvopab 4429	. . . 4 |- `'{<.x, y>. | ((x e. A /\ y e. A) /\ x C_ y)} = {<.y, x>. | ((x e. A /\ y e. A) /\ x C_ y)}
11	10	dmeqi 4284	. . 3 |- dom `'{<.x, y>. | ((x e. A /\ y e. A) /\ x C_ y)} = dom {<.y, x>. | ((x e. A /\ y e. A) /\ x C_ y)}
12		simplr 811	. . . . . . . 8 |- (((x e. A /\ y e. A) /\ x C_ y) -> y e. A)
13		simpll 810	. . . . . . . . 9 |- (((x e. A /\ y e. A) /\ x C_ y) -> x e. A)
14		simpr 442	. . . . . . . . 9 |- (((x e. A /\ y e. A) /\ x C_ y) -> x C_ y)
15	13, 14	jca 494	. . . . . . . 8 |- (((x e. A /\ y e. A) /\ x C_ y) -> (x e. A /\ x C_ y))
16	12, 15	jca 494	. . . . . . 7 |- (((x e. A /\ y e. A) /\ x C_ y) -> (y e. A /\ (x e. A /\ x C_ y)))
17		simprl 812	. . . . . . . . 9 |- ((y e. A /\ (x e. A /\ x C_ y)) -> x e. A)
18		simpl 437	. . . . . . . . 9 |- ((y e. A /\ (x e. A /\ x C_ y)) -> y e. A)
19	17, 18	jca 494	. . . . . . . 8 |- ((y e. A /\ (x e. A /\ x C_ y)) -> (x e. A /\ y e. A))
20		simprr 813	. . . . . . . 8 |- ((y e. A /\ (x e. A /\ x C_ y)) -> x C_ y)
21	19, 20	jca 494	. . . . . . 7 |- ((y e. A /\ (x e. A /\ x C_ y)) -> ((x e. A /\ y e. A) /\ x C_ y))
22	16, 21	impbii 223	. . . . . 6 |- (((x e. A /\ y e. A) /\ x C_ y) <-> (y e. A /\ (x e. A /\ x C_ y)))
23	22	opabbii 3570	. . . . 5 |- {<.y, x>. | ((x e. A /\ y e. A) /\ x C_ y)} = {<.y, x>. | (y e. A /\ (x e. A /\ x C_ y))}
24	23	dmeqi 4284	. . . 4 |- dom {<.y, x>. | ((x e. A /\ y e. A) /\ x C_ y)} = dom {<.y, x>. | (y e. A /\ (x e. A /\ x C_ y))}
25		ssid 2863	. . . . . . 7 |- y C_ y
26		sseq1 2865	. . . . . . . . . 10 |- (x = y -> (x C_ y <-> y C_ y))
27	26	rcla4ev 2620	. . . . . . . . 9 |- ((y e. A /\ y C_ y) -> E.x e. A x C_ y)
28	27	ancoms 416	. . . . . . . 8 |- ((y C_ y /\ y e. A) -> E.x e. A x C_ y)
29		df-rex 2360	. . . . . . . 8 |- (E.x e. A x C_ y <-> E.x(x e. A /\ x C_ y))
30	28, 29	sylib 242	. . . . . . 7 |- ((y C_ y /\ y e. A) -> E.x(x e. A /\ x C_ y))
31	25, 30	mpan 677	. . . . . 6 |- (y e. A -> E.x(x e. A /\ x C_ y))
32	31	rgen 2410	. . . . 5 |- A.y e. A E.x(x e. A /\ x C_ y)
33		dmopab3 4294	. . . . 5 |- (A.y e. A E.x(x e. A /\ x C_ y) <-> dom {<.y, x>. | (y e. A /\ (x e. A /\ x C_ y))} = A)
34	32, 33	mpbi 272	. . . 4 |- dom {<.y, x>. | (y e. A /\ (x e. A /\ x C_ y))} = A
35	24, 34	eqtri 2161	. . 3 |- dom {<.y, x>. | ((x e. A /\ y e. A) /\ x C_ y)} = A
36	9, 11, 35	3eqtri 2165	. 2 |- ran {<.x, y>. | ((x e. A /\ y e. A) /\ x C_ y)} = A
37	4, 8, 36	3eqtri 2165	1 |- ran ( C i^i (A X. A)) = A

Syntax hints:   /\ wa 337   = wceq 1586   e. wcel 1588  E.wex 1615  A.wral 2355  E.wrex 2356   i^i cin 2826   C_ wss 2827  {copab 3565   X. cxp 4117  `'ccnv 4118  dom cdm 4119  ran crn 4120

This theorem is referenced by:  toplat 15377

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-br 3508  df-opab 3566  df-xp 4133  df-rel 4134  df-cnv 4135  df-dm 4137  df-rn 4138

Copyright terms: Public domain