Theorem sbthlem1 6204

Description: Lemma for sbth 6207. Set up similarity with a range. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 11-Mar-2015.)

Hypotheses

Ref	Expression
sbthlem1.1	|- R e. _V
sbthlem1.2	|- X e. _V
sbthlem1.3	|- G = Clos1 ((X \ ran R), R)
sbthlem1.4	|- A = (X i^i G)
sbthlem1.5	|- B = (X \ G)
sbthlem1.6	|- C = (ran R i^i G)
sbthlem1.7	|- D = (ran R \ G)

Assertion

Ref	Expression
sbthlem1	|- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> ran R ~~ X)

Proof of Theorem sbthlem1

Step	Hyp	Ref	Expression
1		df-f1 4793	. . . . . . . . 9 |- (R:dom R-1-1->ran R <-> (R:dom R-->ran R /\ Fun `'R))
2		ssid 3291	. . . . . . . . . . . 12 |- ran R C_ ran R
3		df-f 4792	. . . . . . . . . . . 12 |- (R:dom R-->ran R <-> (R Fn dom R /\ ran R C_ ran R))
4	2, 3	mpbiran2 885	. . . . . . . . . . 11 |- (R:dom R-->ran R <-> R Fn dom R)
5		funfn 5137	. . . . . . . . . . 11 |- (Fun R <-> R Fn dom R)
6	4, 5	bitr4i 243	. . . . . . . . . 10 |- (R:dom R-->ran R <-> Fun R)
7	6	anbi1i 676	. . . . . . . . 9 |- ((R:dom R-->ran R /\ Fun `'R) <-> (Fun R /\ Fun `'R))
8	1, 7	bitri 240	. . . . . . . 8 |- (R:dom R-1-1->ran R <-> (Fun R /\ Fun `'R))
9	8	biimpri 197	. . . . . . 7 |- ((Fun R /\ Fun `'R) -> R:dom R-1-1->ran R)
10		sbthlem1.4	. . . . . . . . 9 |- A = (X i^i G)
11		inss1 3476	. . . . . . . . . 10 |- (X i^i G) C_ X
12		sstr 3281	. . . . . . . . . 10 |- (((X i^i G) C_ X /\ X C_ dom R) -> (X i^i G) C_ dom R)
13	11, 12	mpan 651	. . . . . . . . 9 |- (X C_ dom R -> (X i^i G) C_ dom R)
14	10, 13	syl5eqss 3316	. . . . . . . 8 |- (X C_ dom R -> A C_ dom R)
15	14	adantr 451	. . . . . . 7 |- ((X C_ dom R /\ ran R C_ X) -> A C_ dom R)
16		f1ores 5301	. . . . . . 7 |- ((R:dom R-1-1->ran R /\ A C_ dom R) -> (R |` A):A-1-1-onto->(R"A))
17	9, 15, 16	syl2an 463	. . . . . 6 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (R |` A):A-1-1-onto->(R"A))
18		sbthlem1.1	. . . . . . . 8 |- R e. _V
19		sbthlem1.2	. . . . . . . . . 10 |- X e. _V
20		sbthlem1.3	. . . . . . . . . . 11 |- G = Clos1 ((X \ ran R), R)
21	18	rnex 5108	. . . . . . . . . . . . 13 |- ran R e. _V
22	19, 21	difex 4108	. . . . . . . . . . . 12 |- (X \ ran R) e. _V
23	22, 18	clos1ex 5877	. . . . . . . . . . 11 |- Clos1 ((X \ ran R), R) e. _V
24	20, 23	eqeltri 2423	. . . . . . . . . 10 |- G e. _V
25	19, 24	inex 4106	. . . . . . . . 9 |- (X i^i G) e. _V
26	10, 25	eqeltri 2423	. . . . . . . 8 |- A e. _V
27	18, 26	resex 5118	. . . . . . 7 |- (R |` A) e. _V
28	27	f1oen 6034	. . . . . 6 |- ((R |` A):A-1-1-onto->(R"A) -> A ~~ (R"A))
29	17, 28	syl 15	. . . . 5 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> A ~~ (R"A))
30		sbthlem1.6	. . . . . . . . 9 |- C = (ran R i^i G)
31	22, 18, 20	clos1baseima 5884	. . . . . . . . . 10 |- G = ((X \ ran R) u. (R"G))
32	31	ineq2i 3455	. . . . . . . . 9 |- (ran R i^i G) = (ran R i^i ((X \ ran R) u. (R"G)))
33		indi 3502	. . . . . . . . . 10 |- (ran R i^i ((X \ ran R) u. (R"G))) = ((ran R i^i (X \ ran R)) u. (ran R i^i (R"G)))
34		disjdif 3623	. . . . . . . . . . 11 |- (ran R i^i (X \ ran R)) = (/)
35	34	uneq1i 3415	. . . . . . . . . 10 |- ((ran R i^i (X \ ran R)) u. (ran R i^i (R"G))) = ((/) u. (ran R i^i (R"G)))
36		uncom 3409	. . . . . . . . . . 11 |- ((/) u. (ran R i^i (R"G))) = ((ran R i^i (R"G)) u. (/))
37		un0 3576	. . . . . . . . . . 11 |- ((ran R i^i (R"G)) u. (/)) = (ran R i^i (R"G))
38	36, 37	eqtri 2373	. . . . . . . . . 10 |- ((/) u. (ran R i^i (R"G))) = (ran R i^i (R"G))
39	33, 35, 38	3eqtri 2377	. . . . . . . . 9 |- (ran R i^i ((X \ ran R) u. (R"G))) = (ran R i^i (R"G))
40	30, 32, 39	3eqtri 2377	. . . . . . . 8 |- C = (ran R i^i (R"G))
41		inss2 3477	. . . . . . . . 9 |- (ran R i^i (R"G)) C_ (R"G)
42	41	a1i 10	. . . . . . . 8 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (ran R i^i (R"G)) C_ (R"G))
43	40, 42	syl5eqss 3316	. . . . . . 7 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> C C_ (R"G))
44		imassrn 5010	. . . . . . . . . . . . . 14 |- (R"G) C_ ran R
45		simprr 733	. . . . . . . . . . . . . 14 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> ran R C_ X)
46	44, 45	syl5ss 3284	. . . . . . . . . . . . 13 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (R"G) C_ X)
47		difss 3394	. . . . . . . . . . . . 13 |- (X \ ran R) C_ X
48	46, 47	jctil 523	. . . . . . . . . . . 12 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> ((X \ ran R) C_ X /\ (R"G) C_ X))
49		unss 3438	. . . . . . . . . . . 12 |- (((X \ ran R) C_ X /\ (R"G) C_ X) <-> ((X \ ran R) u. (R"G)) C_ X)
50	48, 49	sylib 188	. . . . . . . . . . 11 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> ((X \ ran R) u. (R"G)) C_ X)
51	31, 50	syl5eqss 3316	. . . . . . . . . 10 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> G C_ X)
52		sseqin2 3475	. . . . . . . . . 10 |- (G C_ X <-> (X i^i G) = G)
53	51, 52	sylib 188	. . . . . . . . 9 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (X i^i G) = G)
54	10, 53	syl5eq 2397	. . . . . . . 8 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> A = G)
55	54	imaeq2d 4943	. . . . . . 7 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (R"A) = (R"G))
56	43, 55	sseqtr4d 3309	. . . . . 6 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> C C_ (R"A))
57		ssun2 3428	. . . . . . . . . . 11 |- (R"G) C_ ((X \ ran R) u. (R"G))
58	57, 31	sseqtr4i 3305	. . . . . . . . . 10 |- (R"G) C_ G
59	55	sseq1d 3299	. . . . . . . . . 10 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> ((R"A) C_ G <-> (R"G) C_ G))
60	58, 59	mpbiri 224	. . . . . . . . 9 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (R"A) C_ G)
61		imassrn 5010	. . . . . . . . 9 |- (R"A) C_ ran R
62	60, 61	jctil 523	. . . . . . . 8 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> ((R"A) C_ ran R /\ (R"A) C_ G))
63		ssin 3478	. . . . . . . 8 |- (((R"A) C_ ran R /\ (R"A) C_ G) <-> (R"A) C_ (ran R i^i G))
64	62, 63	sylib 188	. . . . . . 7 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (R"A) C_ (ran R i^i G))
65	64, 30	syl6sseqr 3319	. . . . . 6 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (R"A) C_ C)
66	56, 65	eqssd 3290	. . . . 5 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> C = (R"A))
67	29, 66	breqtrrd 4666	. . . 4 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> A ~~ C)
68		sbthlem1.5	. . . . . . 7 |- B = (X \ G)
69	19, 24	difex 4108	. . . . . . 7 |- (X \ G) e. _V
70	68, 69	eqeltri 2423	. . . . . 6 |- B e. _V
71	70	enrflx 6036	. . . . 5 |- B ~~ B
72		difsscompl 3550	. . . . . . . . . 10 |- (X \ G) C_ ∼ G
73	72	a1i 10	. . . . . . . . 9 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (X \ G) C_ ∼ G)
74		df-dif 3216	. . . . . . . . . . 11 |- (X \ G) = (X i^i ∼ G)
75	20	clos1base 5879	. . . . . . . . . . . . . 14 |- (X \ ran R) C_ G
76		sscon34 3662	. . . . . . . . . . . . . 14 |- ((X \ ran R) C_ G <-> ∼ G C_ ∼ (X \ ran R))
77	75, 76	mpbi 199	. . . . . . . . . . . . 13 |- ∼ G C_ ∼ (X \ ran R)
78		df-dif 3216	. . . . . . . . . . . . . . 15 |- (X \ ran R) = (X i^i ∼ ran R)
79	78	compleqi 3245	. . . . . . . . . . . . . 14 |- ∼ (X \ ran R) = ∼ (X i^i ∼ ran R)
80		iinun 3549	. . . . . . . . . . . . . 14 |- ∼ (X i^i ∼ ran R) = ( ∼ X u. ∼ ∼ ran R)
81		dblcompl 3228	. . . . . . . . . . . . . . 15 |- ∼ ∼ ran R = ran R
82	81	uneq2i 3416	. . . . . . . . . . . . . 14 |- ( ∼ X u. ∼ ∼ ran R) = ( ∼ X u. ran R)
83	79, 80, 82	3eqtri 2377	. . . . . . . . . . . . 13 |- ∼ (X \ ran R) = ( ∼ X u. ran R)
84	77, 83	sseqtri 3304	. . . . . . . . . . . 12 |- ∼ G C_ ( ∼ X u. ran R)
85		sslin 3482	. . . . . . . . . . . 12 |- ( ∼ G C_ ( ∼ X u. ran R) -> (X i^i ∼ G) C_ (X i^i ( ∼ X u. ran R)))
86	84, 85	ax-mp 5	. . . . . . . . . . 11 |- (X i^i ∼ G) C_ (X i^i ( ∼ X u. ran R))
87	74, 86	eqsstri 3302	. . . . . . . . . 10 |- (X \ G) C_ (X i^i ( ∼ X u. ran R))
88		indi 3502	. . . . . . . . . . . 12 |- (X i^i ( ∼ X u. ran R)) = ((X i^i ∼ X) u. (X i^i ran R))
89		incompl 4074	. . . . . . . . . . . . 13 |- (X i^i ∼ X) = (/)
90	89	uneq1i 3415	. . . . . . . . . . . 12 |- ((X i^i ∼ X) u. (X i^i ran R)) = ((/) u. (X i^i ran R))
91		uncom 3409	. . . . . . . . . . . . 13 |- ((/) u. (X i^i ran R)) = ((X i^i ran R) u. (/))
92		un0 3576	. . . . . . . . . . . . 13 |- ((X i^i ran R) u. (/)) = (X i^i ran R)
93	91, 92	eqtri 2373	. . . . . . . . . . . 12 |- ((/) u. (X i^i ran R)) = (X i^i ran R)
94	88, 90, 93	3eqtri 2377	. . . . . . . . . . 11 |- (X i^i ( ∼ X u. ran R)) = (X i^i ran R)
95		inss2 3477	. . . . . . . . . . 11 |- (X i^i ran R) C_ ran R
96	94, 95	eqsstri 3302	. . . . . . . . . 10 |- (X i^i ( ∼ X u. ran R)) C_ ran R
97	87, 96	sstri 3282	. . . . . . . . 9 |- (X \ G) C_ ran R
98	73, 97	jctil 523	. . . . . . . 8 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> ((X \ G) C_ ran R /\ (X \ G) C_ ∼ G))
99		ssin 3478	. . . . . . . 8 |- (((X \ G) C_ ran R /\ (X \ G) C_ ∼ G) <-> (X \ G) C_ (ran R i^i ∼ G))
100	98, 99	sylib 188	. . . . . . 7 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (X \ G) C_ (ran R i^i ∼ G))
101		sbthlem1.7	. . . . . . . 8 |- D = (ran R \ G)
102		df-dif 3216	. . . . . . . 8 |- (ran R \ G) = (ran R i^i ∼ G)
103	101, 102	eqtri 2373	. . . . . . 7 |- D = (ran R i^i ∼ G)
104	100, 68, 103	3sstr4g 3313	. . . . . 6 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> B C_ D)
105		ssdif 3402	. . . . . . . 8 |- (ran R C_ X -> (ran R \ G) C_ (X \ G))
106	45, 105	syl 15	. . . . . . 7 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (ran R \ G) C_ (X \ G))
107	106, 101, 68	3sstr4g 3313	. . . . . 6 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> D C_ B)
108	104, 107	eqssd 3290	. . . . 5 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> B = D)
109	71, 108	syl5breq 4675	. . . 4 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> B ~~ D)
110	10, 68	ineq12i 3456	. . . . . 6 |- (A i^i B) = ((X i^i G) i^i (X \ G))
111		inindif 4076	. . . . . 6 |- ((X i^i G) i^i (X \ G)) = (/)
112	110, 111	eqtri 2373	. . . . 5 |- (A i^i B) = (/)
113	30, 101	ineq12i 3456	. . . . . 6 |- (C i^i D) = ((ran R i^i G) i^i (ran R \ G))
114		inindif 4076	. . . . . 6 |- ((ran R i^i G) i^i (ran R \ G)) = (/)
115	113, 114	eqtri 2373	. . . . 5 |- (C i^i D) = (/)
116		unen 6049	. . . . 5 |- (((A ~~ C /\ B ~~ D) /\ ((A i^i B) = (/) /\ (C i^i D) = (/))) -> (A u. B) ~~ (C u. D))
117	112, 115, 116	mpanr12 666	. . . 4 |- ((A ~~ C /\ B ~~ D) -> (A u. B) ~~ (C u. D))
118	67, 109, 117	syl2anc 642	. . 3 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (A u. B) ~~ (C u. D))
119		ensym 6038	. . 3 |- ((A u. B) ~~ (C u. D) <-> (C u. D) ~~ (A u. B))
120	118, 119	sylib 188	. 2 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> (C u. D) ~~ (A u. B))
121	30, 101	uneq12i 3417	. . 3 |- (C u. D) = ((ran R i^i G) u. (ran R \ G))
122		inundif 3629	. . 3 |- ((ran R i^i G) u. (ran R \ G)) = ran R
123	121, 122	eqtri 2373	. 2 |- (C u. D) = ran R
124	10, 68	uneq12i 3417	. . 3 |- (A u. B) = ((X i^i G) u. (X \ G))
125		inundif 3629	. . 3 |- ((X i^i G) u. (X \ G)) = X
126	124, 125	eqtri 2373	. 2 |- (A u. B) = X
127	120, 123, 126	3brtr3g 4671	1 |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> ran R ~~ X)

Syntax hints:   -> wi 4   /\ wa 358   = wceq 1642   e. wcel 1710  _Vcvv 2860   ∼ ccompl 3206   \ cdif 3207   u. cun 3208   i^i cin 3209   C_ wss 3258  (/)c0 3551   class class class wbr 4640  "cima 4723  `'ccnv 4772  dom cdm 4773  ran crn 4774   |` cres 4775  Fun wfun 4776   Fn wfn 4777  -->wf 4778  -1-1->wf1 4779  -1-1-onto->wf1o 4781   Clos1 cclos1 5873   ~~ cen 6029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-swap 4725  df-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-dm 4788  df-res 4789  df-fun 4790  df-fn 4791  df-f 4792  df-f1 4793  df-fo 4794  df-f1o 4795  df-2nd 4798  df-txp 5737  df-fix 5741  df-ins2 5751  df-ins3 5753  df-image 5755  df-clos1 5874  df-en 6030

This theorem is referenced by:  sbthlem2  6205