Theorem infmap2lem2 8849

Description: Lemma for infmap2 8850. Given the relation R, we use the Axiom of Choice ac7g 5911 to extract a function f that provides the one-to-one mapping for the dominance relation.

Hypotheses

Ref	Expression
infmap2lem.1	|- A e. _V
infmap2lem.2	|- B e. _V
infmap2lem.3	|- R = {<.z, w>. | ((z C_ A /\ z ~~ B) /\ w:B-onto->z)}

Assertion

Ref	Expression
infmap2lem2	|- {x | (x C_ A /\ x ~~ B)} ~<_ (A ^m B)

Distinct variable groups:   x,z,w,A   x,B,z,w

Proof of Theorem infmap2lem2

Step	Hyp	Ref	Expression
1		infmap2lem.3	. . . 4 |- R = {<.z, w>. | ((z C_ A /\ z ~~ B) /\ w:B-onto->z)}
2		df-xp 4000	. . . . . 6 |- (~PA X. (A ^m B)) = {<.z, w>. | (z e. ~PA /\ w e. (A ^m B))}
3		infmap2lem.1	. . . . . . . 8 |- A e. _V
4	3	pwex 3487	. . . . . . 7 |- ~PA e. _V
5		oprex 4907	. . . . . . 7 |- (A ^m B) e. _V
6	4, 5	xpex 4096	. . . . . 6 |- (~PA X. (A ^m B)) e. _V
7	2, 6	eqeltrri 1968	. . . . 5 |- {<.z, w>. | (z e. ~PA /\ w e. (A ^m B))} e. _V
8		simpl 346	. . . . . . . . 9 |- ((z C_ A /\ w:B-onto->z) -> z C_ A)
9		visset 2295	. . . . . . . . . 10 |- z e. _V
10	9	elpw 3037	. . . . . . . . 9 |- (z e. ~PA <-> z C_ A)
11	8, 10	sylibr 217	. . . . . . . 8 |- ((z C_ A /\ w:B-onto->z) -> z e. ~PA)
12		infmap2lem.2	. . . . . . . . . . 11 |- B e. _V
13	3, 12	elmap 5393	. . . . . . . . . 10 |- (w e. (A ^m B) <-> w:B-->A)
14		df-f 4010	. . . . . . . . . 10 |- (w:B-->A <-> (w Fn B /\ ran w C_ A))
15	13, 14	bitri 190	. . . . . . . . 9 |- (w e. (A ^m B) <-> (w Fn B /\ ran w C_ A))
16		fofn 4619	. . . . . . . . . 10 |- (w:B-onto->z -> w Fn B)
17	16	adantl 424	. . . . . . . . 9 |- ((z C_ A /\ w:B-onto->z) -> w Fn B)
18		forn 4620	. . . . . . . . . . 11 |- (w:B-onto->z -> ran w = z)
19	18	sseq1d 2644	. . . . . . . . . 10 |- (w:B-onto->z -> (ran w C_ A <-> z C_ A))
20	19	biimparc 463	. . . . . . . . 9 |- ((z C_ A /\ w:B-onto->z) -> ran w C_ A)
21	15, 17, 20	sylanbrc 527	. . . . . . . 8 |- ((z C_ A /\ w:B-onto->z) -> w e. (A ^m B))
22	11, 21	jca 310	. . . . . . 7 |- ((z C_ A /\ w:B-onto->z) -> (z e. ~PA /\ w e. (A ^m B)))
23	22	adantlr 429	. . . . . 6 |- (((z C_ A /\ z ~~ B) /\ w:B-onto->z) -> (z e. ~PA /\ w e. (A ^m B)))
24	23	ssopab2i 3574	. . . . 5 |- {<.z, w>. | ((z C_ A /\ z ~~ B) /\ w:B-onto->z)} C_ {<.z, w>. | (z e. ~PA /\ w e. (A ^m B))}
25	7, 24	ssexi 3456	. . . 4 |- {<.z, w>. | ((z C_ A /\ z ~~ B) /\ w:B-onto->z)} e. _V
26	1, 25	eqeltri 1967	. . 3 |- R e. _V
27		ac7g 5911	. . 3 |- (R e. _V -> E.f(f C_ R /\ f Fn dom R))
28	26, 27	ax-mp 7	. 2 |- E.f(f C_ R /\ f Fn dom R)
29		df-pw 3035	. . . . . 6 |- ~PA = {x | x C_ A}
30	29, 4	eqeltrri 1968	. . . . 5 |- {x | x C_ A} e. _V
31		simpl 346	. . . . . 6 |- ((x C_ A /\ x ~~ B) -> x C_ A)
32	31	ss2abi 2679	. . . . 5 |- {x | (x C_ A /\ x ~~ B)} C_ {x | x C_ A}
33	30, 32	ssexi 3456	. . . 4 |- {x | (x C_ A /\ x ~~ B)} e. _V
34	3, 12, 1	infmap2lem1 8848	. . . . . 6 |- ((f C_ R /\ f Fn dom R) -> (v e. {x | (x C_ A /\ x ~~ B)} -> (v C_ A /\ (f` v):B-onto->v)))
35		fss 4571	. . . . . . . . 9 |- (((f` v):B-->v /\ v C_ A) -> (f` v):B-->A)
36		fof 4617	. . . . . . . . 9 |- ((f` v):B-onto->v -> (f` v):B-->v)
37	35, 36	sylan 497	. . . . . . . 8 |- (((f` v):B-onto->v /\ v C_ A) -> (f` v):B-->A)
38	37	ancoms 484	. . . . . . 7 |- ((v C_ A /\ (f` v):B-onto->v) -> (f` v):B-->A)
39	3, 12	elmap 5393	. . . . . . 7 |- ((f` v) e. (A ^m B) <-> (f` v):B-->A)
40	38, 39	sylibr 217	. . . . . 6 |- ((v C_ A /\ (f` v):B-onto->v) -> (f` v) e. (A ^m B))
41	34, 40	syl6 25	. . . . 5 |- ((f C_ R /\ f Fn dom R) -> (v e. {x | (x C_ A /\ x ~~ B)} -> (f` v) e. (A ^m B)))
42		simpr 350	. . . . . . . 8 |- ((v C_ A /\ (f` v):B-onto->v) -> (f` v):B-onto->v)
43	34, 42	syl6 25	. . . . . . 7 |- ((f C_ R /\ f Fn dom R) -> (v e. {x | (x C_ A /\ x ~~ B)} -> (f` v):B-onto->v))
44	3, 12, 1	infmap2lem1 8848	. . . . . . . 8 |- ((f C_ R /\ f Fn dom R) -> (u e. {x | (x C_ A /\ x ~~ B)} -> (u C_ A /\ (f` u):B-onto->u)))
45		simpr 350	. . . . . . . 8 |- ((u C_ A /\ (f` u):B-onto->u) -> (f` u):B-onto->u)
46	44, 45	syl6 25	. . . . . . 7 |- ((f C_ R /\ f Fn dom R) -> (u e. {x | (x C_ A /\ x ~~ B)} -> (f` u):B-onto->u))
47	43, 46	anim12d 617	. . . . . 6 |- ((f C_ R /\ f Fn dom R) -> ((v e. {x | (x C_ A /\ x ~~ B)} /\ u e. {x | (x C_ A /\ x ~~ B)}) -> ((f` v):B-onto->v /\ (f` u):B-onto->u)))
48		forn 4620	. . . . . . . . 9 |- ((f` v):B-onto->v -> ran ( f` v) = v)
49		forn 4620	. . . . . . . . 9 |- ((f` u):B-onto->u -> ran ( f` u) = u)
50	48, 49	eqeqan12d 1901	. . . . . . . 8 |- (((f` v):B-onto->v /\ (f` u):B-onto->u) -> (ran ( f` v) = ran ( f` u) <-> v = u))
51		rneq 4186	. . . . . . . 8 |- ((f` v) = (f` u) -> ran ( f` v) = ran ( f` u))
52	50, 51	syl5bi 225	. . . . . . 7 |- (((f` v):B-onto->v /\ (f` u):B-onto->u) -> ((f` v) = (f` u) -> v = u))
53		fveq2 4681	. . . . . . 7 |- (v = u -> (f` v) = (f` u))
54	52, 53	impbid1 575	. . . . . 6 |- (((f` v):B-onto->v /\ (f` u):B-onto->u) -> ((f` v) = (f` u) <-> v = u))
55	47, 54	syl6 25	. . . . 5 |- ((f C_ R /\ f Fn dom R) -> ((v e. {x | (x C_ A /\ x ~~ B)} /\ u e. {x | (x C_ A /\ x ~~ B)}) -> ((f` v) = (f` u) <-> v = u)))
56	41, 55	dom2d 5463	. . . 4 |- ((f C_ R /\ f Fn dom R) -> ({x | (x C_ A /\ x ~~ B)} e. _V -> {x | (x C_ A /\ x ~~ B)} ~<_ (A ^m B)))
57	33, 56	mpi 55	. . 3 |- ((f C_ R /\ f Fn dom R) -> {x | (x C_ A /\ x ~~ B)} ~<_ (A ^m B))
58	57	19.23aiv 1674	. 2 |- (E.f(f C_ R /\ f Fn dom R) -> {x | (x C_ A /\ x ~~ B)} ~<_ (A ^m B))
59	28, 58	ax-mp 7	1 |- {x | (x C_ A /\ x ~~ B)} ~<_ (A ^m B)

Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  _Vcvv 2292   C_ wss 2593  ~Pcpw 3032   class class class wbr 3338  {copab 3395   X. cxp 3984  dom cdm 3986  ran crn 3987   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` cfv 3998  (class class class)co 4884   ^m cmap 5381   ~~ cen 5423   ~<_ cdom 5424

This theorem is referenced by:  infmap2 8850

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-er 5318  df-map 5383  df-en 5427  df-dom 5428

Copyright terms: Public domain