Theorem sbthlem3 6206

Description: Lemma for sbth 6207. If A is equinumerous with a subset of B and vice-versa, then A is equinumerous with B. Theorem XI.1.15 of [Rosser] p. 353. (Contributed by SF, 10-Mar-2015.)

Assertion

Ref	Expression
sbthlem3	|- (((A ~~ C /\ C C_ B) /\ (B ~~ D /\ D C_ A)) -> A ~~ B)

Proof of Theorem sbthlem3

Dummy variables r s are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bren 6031	. . . . . . 7 |- (A ~~ C <-> E.r r:A-1-1-onto->C)
2		bren 6031	. . . . . . 7 |- (B ~~ D <-> E.s s:B-1-1-onto->D)
3	1, 2	anbi12i 678	. . . . . 6 |- ((A ~~ C /\ B ~~ D) <-> (E.r r:A-1-1-onto->C /\ E.s s:B-1-1-onto->D))
4		eeanv 1913	. . . . . 6 |- (E.rE.s(r:A-1-1-onto->C /\ s:B-1-1-onto->D) <-> (E.r r:A-1-1-onto->C /\ E.s s:B-1-1-onto->D))
5	3, 4	bitr4i 243	. . . . 5 |- ((A ~~ C /\ B ~~ D) <-> E.rE.s(r:A-1-1-onto->C /\ s:B-1-1-onto->D))
6		simprl 732	. . . . . . . . . . . 12 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> C C_ B)
7		f1ofo 5294	. . . . . . . . . . . . . 14 |- (r:A-1-1-onto->C -> r:A-onto->C)
8		forn 5273	. . . . . . . . . . . . . 14 |- (r:A-onto->C -> ran r = C)
9	7, 8	syl 15	. . . . . . . . . . . . 13 |- (r:A-1-1-onto->C -> ran r = C)
10	9	ad2antrr 706	. . . . . . . . . . . 12 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> ran r = C)
11		f1odm 5291	. . . . . . . . . . . . 13 |- (s:B-1-1-onto->D -> dom s = B)
12	11	ad2antlr 707	. . . . . . . . . . . 12 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> dom s = B)
13	6, 10, 12	3sstr4d 3315	. . . . . . . . . . 11 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> ran r C_ dom s)
14		dmcosseq 4974	. . . . . . . . . . 11 |- (ran r C_ dom s -> dom (s o. r) = dom r)
15	13, 14	syl 15	. . . . . . . . . 10 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> dom (s o. r) = dom r)
16		f1odm 5291	. . . . . . . . . . 11 |- (r:A-1-1-onto->C -> dom r = A)
17	16	ad2antrr 706	. . . . . . . . . 10 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> dom r = A)
18	15, 17	eqtrd 2385	. . . . . . . . 9 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> dom (s o. r) = A)
19		f1ofun 5290	. . . . . . . . . . . . . 14 |- (s:B-1-1-onto->D -> Fun s)
20		f1ofun 5290	. . . . . . . . . . . . . 14 |- (r:A-1-1-onto->C -> Fun r)
21		funco 5143	. . . . . . . . . . . . . 14 |- ((Fun s /\ Fun r) -> Fun (s o. r))
22	19, 20, 21	syl2anr 464	. . . . . . . . . . . . 13 |- ((r:A-1-1-onto->C /\ s:B-1-1-onto->D) -> Fun (s o. r))
23		dff1o2 5292	. . . . . . . . . . . . . . . 16 |- (r:A-1-1-onto->C <-> (r Fn A /\ Fun `'r /\ ran r = C))
24	23	simp2bi 971	. . . . . . . . . . . . . . 15 |- (r:A-1-1-onto->C -> Fun `'r)
25		dff1o2 5292	. . . . . . . . . . . . . . . 16 |- (s:B-1-1-onto->D <-> (s Fn B /\ Fun `'s /\ ran s = D))
26	25	simp2bi 971	. . . . . . . . . . . . . . 15 |- (s:B-1-1-onto->D -> Fun `'s)
27		funco 5143	. . . . . . . . . . . . . . 15 |- ((Fun `'r /\ Fun `'s) -> Fun (`'r o. `'s))
28	24, 26, 27	syl2an 463	. . . . . . . . . . . . . 14 |- ((r:A-1-1-onto->C /\ s:B-1-1-onto->D) -> Fun (`'r o. `'s))
29		cnvco 4895	. . . . . . . . . . . . . . 15 |- `'(s o. r) = (`'r o. `'s)
30	29	funeqi 5129	. . . . . . . . . . . . . 14 |- (Fun `'(s o. r) <-> Fun (`'r o. `'s))
31	28, 30	sylibr 203	. . . . . . . . . . . . 13 |- ((r:A-1-1-onto->C /\ s:B-1-1-onto->D) -> Fun `'(s o. r))
32	22, 31	jca 518	. . . . . . . . . . . 12 |- ((r:A-1-1-onto->C /\ s:B-1-1-onto->D) -> (Fun (s o. r) /\ Fun `'(s o. r)))
33	32	adantr 451	. . . . . . . . . . 11 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> (Fun (s o. r) /\ Fun `'(s o. r)))
34		dff1o2 5292	. . . . . . . . . . . 12 |- ((s o. r):dom (s o. r)-1-1-onto->ran (s o. r) <-> ((s o. r) Fn dom (s o. r) /\ Fun `'(s o. r) /\ ran (s o. r) = ran (s o. r)))
35		funfn 5137	. . . . . . . . . . . . . 14 |- (Fun (s o. r) <-> (s o. r) Fn dom (s o. r))
36	35	anbi1i 676	. . . . . . . . . . . . 13 |- ((Fun (s o. r) /\ Fun `'(s o. r)) <-> ((s o. r) Fn dom (s o. r) /\ Fun `'(s o. r)))
37		eqid 2353	. . . . . . . . . . . . . 14 |- ran (s o. r) = ran (s o. r)
38		df-3an 936	. . . . . . . . . . . . . 14 |- (((s o. r) Fn dom (s o. r) /\ Fun `'(s o. r) /\ ran (s o. r) = ran (s o. r)) <-> (((s o. r) Fn dom (s o. r) /\ Fun `'(s o. r)) /\ ran (s o. r) = ran (s o. r)))
39	37, 38	mpbiran2 885	. . . . . . . . . . . . 13 |- (((s o. r) Fn dom (s o. r) /\ Fun `'(s o. r) /\ ran (s o. r) = ran (s o. r)) <-> ((s o. r) Fn dom (s o. r) /\ Fun `'(s o. r)))
40	36, 39	bitr4i 243	. . . . . . . . . . . 12 |- ((Fun (s o. r) /\ Fun `'(s o. r)) <-> ((s o. r) Fn dom (s o. r) /\ Fun `'(s o. r) /\ ran (s o. r) = ran (s o. r)))
41	34, 40	bitr4i 243	. . . . . . . . . . 11 |- ((s o. r):dom (s o. r)-1-1-onto->ran (s o. r) <-> (Fun (s o. r) /\ Fun `'(s o. r)))
42	33, 41	sylibr 203	. . . . . . . . . 10 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> (s o. r):dom (s o. r)-1-1-onto->ran (s o. r))
43		vex 2863	. . . . . . . . . . . 12 |- s e. _V
44		vex 2863	. . . . . . . . . . . 12 |- r e. _V
45	43, 44	coex 4751	. . . . . . . . . . 11 |- (s o. r) e. _V
46	45	f1oen 6034	. . . . . . . . . 10 |- ((s o. r):dom (s o. r)-1-1-onto->ran (s o. r) -> dom (s o. r) ~~ ran (s o. r))
47	42, 46	syl 15	. . . . . . . . 9 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> dom (s o. r) ~~ ran (s o. r))
48	18, 47	eqbrtrrd 4662	. . . . . . . 8 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> A ~~ ran (s o. r))
49		f1ofo 5294	. . . . . . . . . . . 12 |- (s:B-1-1-onto->D -> s:B-onto->D)
50		forn 5273	. . . . . . . . . . . 12 |- (s:B-onto->D -> ran s = D)
51	49, 50	syl 15	. . . . . . . . . . 11 |- (s:B-1-1-onto->D -> ran s = D)
52	43	rnex 5108	. . . . . . . . . . 11 |- ran s e. _V
53	51, 52	syl6eqelr 2442	. . . . . . . . . 10 |- (s:B-1-1-onto->D -> D e. _V)
54	53	ad2antlr 707	. . . . . . . . 9 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> D e. _V)
55		simprr 733	. . . . . . . . . 10 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> D C_ A)
56	55, 18	sseqtr4d 3309	. . . . . . . . 9 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> D C_ dom (s o. r))
57		rncoss 4973	. . . . . . . . . 10 |- ran (s o. r) C_ ran s
58	51	ad2antlr 707	. . . . . . . . . 10 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> ran s = D)
59	57, 58	syl5sseq 3320	. . . . . . . . 9 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> ran (s o. r) C_ D)
60	45	sbthlem2 6205	. . . . . . . . 9 |- (((Fun (s o. r) /\ Fun `'(s o. r)) /\ (D e. _V /\ D C_ dom (s o. r) /\ ran (s o. r) C_ D)) -> ran (s o. r) ~~ D)
61	33, 54, 56, 59, 60	syl13anc 1184	. . . . . . . 8 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> ran (s o. r) ~~ D)
62		entr 6039	. . . . . . . 8 |- ((A ~~ ran (s o. r) /\ ran (s o. r) ~~ D) -> A ~~ D)
63	48, 61, 62	syl2anc 642	. . . . . . 7 |- (((r:A-1-1-onto->C /\ s:B-1-1-onto->D) /\ (C C_ B /\ D C_ A)) -> A ~~ D)
64	63	ex 423	. . . . . 6 |- ((r:A-1-1-onto->C /\ s:B-1-1-onto->D) -> ((C C_ B /\ D C_ A) -> A ~~ D))
65	64	exlimivv 1635	. . . . 5 |- (E.rE.s(r:A-1-1-onto->C /\ s:B-1-1-onto->D) -> ((C C_ B /\ D C_ A) -> A ~~ D))
66	5, 65	sylbi 187	. . . 4 |- ((A ~~ C /\ B ~~ D) -> ((C C_ B /\ D C_ A) -> A ~~ D))
67	66	imp 418	. . 3 |- (((A ~~ C /\ B ~~ D) /\ (C C_ B /\ D C_ A)) -> A ~~ D)
68	67	an4s 799	. 2 |- (((A ~~ C /\ C C_ B) /\ (B ~~ D /\ D C_ A)) -> A ~~ D)
69		ensymi 6037	. . 3 |- (B ~~ D -> D ~~ B)
70	69	ad2antrl 708	. 2 |- (((A ~~ C /\ C C_ B) /\ (B ~~ D /\ D C_ A)) -> D ~~ B)
71		entr 6039	. 2 |- ((A ~~ D /\ D ~~ B) -> A ~~ B)
72	68, 70, 71	syl2anc 642	1 |- (((A ~~ C /\ C C_ B) /\ (B ~~ D /\ D C_ A)) -> A ~~ B)

Syntax hints:   -> wi 4   /\ wa 358   /\ w3a 934  E.wex 1541   = wceq 1642   e. wcel 1710  _Vcvv 2860   C_ wss 3258   class class class wbr 4640   o. ccom 4722  `'ccnv 4772  dom cdm 4773  ran crn 4774  Fun wfun 4776   Fn wfn 4777  -onto->wfo 4780  -1-1-onto->wf1o 4781   ~~ 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:  sbth  6207