New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  sbthlem3 GIF version

Theorem sbthlem3 6205
 Description: Lemma for sbth 6206. 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 (((AC C B) (BD D A)) → AB)

Proof of Theorem sbthlem3
Dummy variables r s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bren 6030 . . . . . . 7 (ACr r:A1-1-ontoC)
2 bren 6030 . . . . . . 7 (BDs s:B1-1-ontoD)
31, 2anbi12i 678 . . . . . 6 ((AC BD) ↔ (r r:A1-1-ontoC s s:B1-1-ontoD))
4 eeanv 1913 . . . . . 6 (rs(r:A1-1-ontoC s:B1-1-ontoD) ↔ (r r:A1-1-ontoC s s:B1-1-ontoD))
53, 4bitr4i 243 . . . . 5 ((AC BD) ↔ rs(r:A1-1-ontoC s:B1-1-ontoD))
6 simprl 732 . . . . . . . . . . . 12 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → C B)
7 f1ofo 5293 . . . . . . . . . . . . . 14 (r:A1-1-ontoCr:AontoC)
8 forn 5272 . . . . . . . . . . . . . 14 (r:AontoC → ran r = C)
97, 8syl 15 . . . . . . . . . . . . 13 (r:A1-1-ontoC → ran r = C)
109ad2antrr 706 . . . . . . . . . . . 12 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → ran r = C)
11 f1odm 5290 . . . . . . . . . . . . 13 (s:B1-1-ontoD → dom s = B)
1211ad2antlr 707 . . . . . . . . . . . 12 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → dom s = B)
136, 10, 123sstr4d 3314 . . . . . . . . . . 11 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → ran r dom s)
14 dmcosseq 4973 . . . . . . . . . . 11 (ran r dom s → dom (s r) = dom r)
1513, 14syl 15 . . . . . . . . . 10 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → dom (s r) = dom r)
16 f1odm 5290 . . . . . . . . . . 11 (r:A1-1-ontoC → dom r = A)
1716ad2antrr 706 . . . . . . . . . 10 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → dom r = A)
1815, 17eqtrd 2385 . . . . . . . . 9 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → dom (s r) = A)
19 f1ofun 5289 . . . . . . . . . . . . . 14 (s:B1-1-ontoD → Fun s)
20 f1ofun 5289 . . . . . . . . . . . . . 14 (r:A1-1-ontoC → Fun r)
21 funco 5142 . . . . . . . . . . . . . 14 ((Fun s Fun r) → Fun (s r))
2219, 20, 21syl2anr 464 . . . . . . . . . . . . 13 ((r:A1-1-ontoC s:B1-1-ontoD) → Fun (s r))
23 dff1o2 5291 . . . . . . . . . . . . . . . 16 (r:A1-1-ontoC ↔ (r Fn A Fun r ran r = C))
2423simp2bi 971 . . . . . . . . . . . . . . 15 (r:A1-1-ontoC → Fun r)
25 dff1o2 5291 . . . . . . . . . . . . . . . 16 (s:B1-1-ontoD ↔ (s Fn B Fun s ran s = D))
2625simp2bi 971 . . . . . . . . . . . . . . 15 (s:B1-1-ontoD → Fun s)
27 funco 5142 . . . . . . . . . . . . . . 15 ((Fun r Fun s) → Fun (r s))
2824, 26, 27syl2an 463 . . . . . . . . . . . . . 14 ((r:A1-1-ontoC s:B1-1-ontoD) → Fun (r s))
29 cnvco 4894 . . . . . . . . . . . . . . 15 (s r) = (r s)
3029funeqi 5128 . . . . . . . . . . . . . 14 (Fun (s r) ↔ Fun (r s))
3128, 30sylibr 203 . . . . . . . . . . . . 13 ((r:A1-1-ontoC s:B1-1-ontoD) → Fun (s r))
3222, 31jca 518 . . . . . . . . . . . 12 ((r:A1-1-ontoC s:B1-1-ontoD) → (Fun (s r) Fun (s r)))
3332adantr 451 . . . . . . . . . . 11 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → (Fun (s r) Fun (s r)))
34 dff1o2 5291 . . . . . . . . . . . 12 ((s r):dom (s r)–1-1-onto→ran (s r) ↔ ((s r) Fn dom (s r) Fun (s r) ran (s r) = ran (s r)))
35 funfn 5136 . . . . . . . . . . . . . 14 (Fun (s r) ↔ (s r) Fn dom (s r))
3635anbi1i 676 . . . . . . . . . . . . 13 ((Fun (s r) Fun (s r)) ↔ ((s r) Fn dom (s r) Fun (s r)))
37 eqid 2353 . . . . . . . . . . . . . 14 ran (s r) = ran (s r)
38 df-3an 936 . . . . . . . . . . . . . 14 (((s r) Fn dom (s r) Fun (s r) ran (s r) = ran (s r)) ↔ (((s r) Fn dom (s r) Fun (s r)) ran (s r) = ran (s r)))
3937, 38mpbiran2 885 . . . . . . . . . . . . 13 (((s r) Fn dom (s r) Fun (s r) ran (s r) = ran (s r)) ↔ ((s r) Fn dom (s r) Fun (s r)))
4036, 39bitr4i 243 . . . . . . . . . . . 12 ((Fun (s r) Fun (s r)) ↔ ((s r) Fn dom (s r) Fun (s r) ran (s r) = ran (s r)))
4134, 40bitr4i 243 . . . . . . . . . . 11 ((s r):dom (s r)–1-1-onto→ran (s r) ↔ (Fun (s r) Fun (s r)))
4233, 41sylibr 203 . . . . . . . . . 10 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → (s r):dom (s r)–1-1-onto→ran (s r))
43 vex 2862 . . . . . . . . . . . 12 s V
44 vex 2862 . . . . . . . . . . . 12 r V
4543, 44coex 4750 . . . . . . . . . . 11 (s r) V
4645f1oen 6033 . . . . . . . . . 10 ((s r):dom (s r)–1-1-onto→ran (s r) → dom (s r) ≈ ran (s r))
4742, 46syl 15 . . . . . . . . 9 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → dom (s r) ≈ ran (s r))
4818, 47eqbrtrrd 4661 . . . . . . . 8 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → A ≈ ran (s r))
49 f1ofo 5293 . . . . . . . . . . . 12 (s:B1-1-ontoDs:BontoD)
50 forn 5272 . . . . . . . . . . . 12 (s:BontoD → ran s = D)
5149, 50syl 15 . . . . . . . . . . 11 (s:B1-1-ontoD → ran s = D)
5243rnex 5107 . . . . . . . . . . 11 ran s V
5351, 52syl6eqelr 2442 . . . . . . . . . 10 (s:B1-1-ontoDD V)
5453ad2antlr 707 . . . . . . . . 9 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → D V)
55 simprr 733 . . . . . . . . . 10 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → D A)
5655, 18sseqtr4d 3308 . . . . . . . . 9 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → D dom (s r))
57 rncoss 4972 . . . . . . . . . 10 ran (s r) ran s
5851ad2antlr 707 . . . . . . . . . 10 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → ran s = D)
5957, 58syl5sseq 3319 . . . . . . . . 9 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → ran (s r) D)
6045sbthlem2 6204 . . . . . . . . 9 (((Fun (s r) Fun (s r)) (D V D dom (s r) ran (s r) D)) → ran (s r) ≈ D)
6133, 54, 56, 59, 60syl13anc 1184 . . . . . . . 8 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → ran (s r) ≈ D)
62 entr 6038 . . . . . . . 8 ((A ≈ ran (s r) ran (s r) ≈ D) → AD)
6348, 61, 62syl2anc 642 . . . . . . 7 (((r:A1-1-ontoC s:B1-1-ontoD) (C B D A)) → AD)
6463ex 423 . . . . . 6 ((r:A1-1-ontoC s:B1-1-ontoD) → ((C B D A) → AD))
6564exlimivv 1635 . . . . 5 (rs(r:A1-1-ontoC s:B1-1-ontoD) → ((C B D A) → AD))
665, 65sylbi 187 . . . 4 ((AC BD) → ((C B D A) → AD))
6766imp 418 . . 3 (((AC BD) (C B D A)) → AD)
6867an4s 799 . 2 (((AC C B) (BD D A)) → AD)
69 ensymi 6036 . . 3 (BDDB)
7069ad2antrl 708 . 2 (((AC C B) (BD D A)) → DB)
71 entr 6038 . 2 ((AD DB) → AB)
7268, 70, 71syl2anc 642 1 (((AC C B) (BD D A)) → AB)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859   ⊆ wss 3257   class class class wbr 4639   ∘ ccom 4721  ◡ccnv 4771  dom cdm 4772  ran crn 4773  Fun wfun 4775   Fn wfn 4776  –onto→wfo 4779  –1-1-onto→wf1o 4780   ≈ cen 6028 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 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087 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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-2nd 4797  df-txp 5736  df-fix 5740  df-ins2 5750  df-ins3 5752  df-image 5754  df-clos1 5873  df-en 6029 This theorem is referenced by:  sbth  6206
 Copyright terms: Public domain W3C validator