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 ⊆ B) ∧ (B ≈ D ∧ D ⊆ 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 ↔ ∃r r:A–1-1-onto→C)
2		bren 6031	. . . . . . 7 ⊢ (B ≈ D ↔ ∃s s:B–1-1-onto→D)
3	1, 2	anbi12i 678	. . . . . 6 ⊢ ((A ≈ C ∧ B ≈ D) ↔ (∃r r:A–1-1-onto→C ∧ ∃s s:B–1-1-onto→D))
4		eeanv 1913	. . . . . 6 ⊢ (∃r∃s(r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ↔ (∃r r:A–1-1-onto→C ∧ ∃s s:B–1-1-onto→D))
5	3, 4	bitr4i 243	. . . . 5 ⊢ ((A ≈ C ∧ B ≈ D) ↔ ∃r∃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 ⊆ B ∧ D ⊆ A)) → 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 ⊆ B ∧ D ⊆ 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 ⊆ B ∧ D ⊆ A)) → dom s = B)
13	6, 10, 12	3sstr4d 3315	. . . . . . . . . . 11 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → ran r ⊆ dom s)
14		dmcosseq 4974	. . . . . . . . . . 11 ⊢ (ran r ⊆ dom s → dom (s ∘ r) = dom r)
15	13, 14	syl 15	. . . . . . . . . 10 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → dom (s ∘ 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 ⊆ B ∧ D ⊆ A)) → dom r = A)
18	15, 17	eqtrd 2385	. . . . . . . . 9 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → dom (s ∘ 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 ∘ r))
22	19, 20, 21	syl2anr 464	. . . . . . . . . . . . 13 ⊢ ((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) → Fun (s ∘ 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 ∘ ◡s))
28	24, 26, 27	syl2an 463	. . . . . . . . . . . . . 14 ⊢ ((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) → Fun (◡r ∘ ◡s))
29		cnvco 4895	. . . . . . . . . . . . . . 15 ⊢ ◡(s ∘ r) = (◡r ∘ ◡s)
30	29	funeqi 5129	. . . . . . . . . . . . . 14 ⊢ (Fun ◡(s ∘ r) ↔ Fun (◡r ∘ ◡s))
31	28, 30	sylibr 203	. . . . . . . . . . . . 13 ⊢ ((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) → Fun ◡(s ∘ r))
32	22, 31	jca 518	. . . . . . . . . . . 12 ⊢ ((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) → (Fun (s ∘ r) ∧ Fun ◡(s ∘ r)))
33	32	adantr 451	. . . . . . . . . . 11 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → (Fun (s ∘ r) ∧ Fun ◡(s ∘ r)))
34		dff1o2 5292	. . . . . . . . . . . 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 5137	. . . . . . . . . . . . . 14 ⊢ (Fun (s ∘ r) ↔ (s ∘ r) Fn dom (s ∘ r))
36	35	anbi1i 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)))
39	37, 38	mpbiran2 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)))
40	36, 39	bitr4i 243	. . . . . . . . . . . 12 ⊢ ((Fun (s ∘ r) ∧ Fun ◡(s ∘ r)) ↔ ((s ∘ r) Fn dom (s ∘ r) ∧ Fun ◡(s ∘ r) ∧ ran (s ∘ r) = ran (s ∘ r)))
41	34, 40	bitr4i 243	. . . . . . . . . . 11 ⊢ ((s ∘ r):dom (s ∘ r)–1-1-onto→ran (s ∘ r) ↔ (Fun (s ∘ r) ∧ Fun ◡(s ∘ r)))
42	33, 41	sylibr 203	. . . . . . . . . 10 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → (s ∘ r):dom (s ∘ r)–1-1-onto→ran (s ∘ r))
43		vex 2863	. . . . . . . . . . . 12 ⊢ s ∈ V
44		vex 2863	. . . . . . . . . . . 12 ⊢ r ∈ V
45	43, 44	coex 4751	. . . . . . . . . . 11 ⊢ (s ∘ r) ∈ V
46	45	f1oen 6034	. . . . . . . . . 10 ⊢ ((s ∘ r):dom (s ∘ r)–1-1-onto→ran (s ∘ r) → dom (s ∘ r) ≈ ran (s ∘ r))
47	42, 46	syl 15	. . . . . . . . 9 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → dom (s ∘ r) ≈ ran (s ∘ r))
48	18, 47	eqbrtrrd 4662	. . . . . . . 8 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → A ≈ ran (s ∘ 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 ∈ V
53	51, 52	syl6eqelr 2442	. . . . . . . . . 10 ⊢ (s:B–1-1-onto→D → D ∈ V)
54	53	ad2antlr 707	. . . . . . . . 9 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → D ∈ V)
55		simprr 733	. . . . . . . . . 10 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → D ⊆ A)
56	55, 18	sseqtr4d 3309	. . . . . . . . 9 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → D ⊆ dom (s ∘ r))
57		rncoss 4973	. . . . . . . . . 10 ⊢ ran (s ∘ r) ⊆ ran s
58	51	ad2antlr 707	. . . . . . . . . 10 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → ran s = D)
59	57, 58	syl5sseq 3320	. . . . . . . . 9 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → ran (s ∘ r) ⊆ D)
60	45	sbthlem2 6205	. . . . . . . . 9 ⊢ (((Fun (s ∘ r) ∧ Fun ◡(s ∘ r)) ∧ (D ∈ V ∧ D ⊆ dom (s ∘ r) ∧ ran (s ∘ r) ⊆ D)) → ran (s ∘ r) ≈ D)
61	33, 54, 56, 59, 60	syl13anc 1184	. . . . . . . 8 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → ran (s ∘ r) ≈ D)
62		entr 6039	. . . . . . . 8 ⊢ ((A ≈ ran (s ∘ r) ∧ ran (s ∘ r) ≈ D) → A ≈ D)
63	48, 61, 62	syl2anc 642	. . . . . . 7 ⊢ (((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) ∧ (C ⊆ B ∧ D ⊆ A)) → A ≈ D)
64	63	ex 423	. . . . . 6 ⊢ ((r:A–1-1-onto→C ∧ s:B–1-1-onto→D) → ((C ⊆ B ∧ D ⊆ A) → A ≈ D))
65	64	exlimivv 1635	. . . . 5 ⊢ (∃r∃s(r:A–1-1-onto→C ∧ s:B–1-1-onto→D) → ((C ⊆ B ∧ D ⊆ A) → A ≈ D))
66	5, 65	sylbi 187	. . . 4 ⊢ ((A ≈ C ∧ B ≈ D) → ((C ⊆ B ∧ D ⊆ A) → A ≈ D))
67	66	imp 418	. . 3 ⊢ (((A ≈ C ∧ B ≈ D) ∧ (C ⊆ B ∧ D ⊆ A)) → A ≈ D)
68	67	an4s 799	. 2 ⊢ (((A ≈ C ∧ C ⊆ B) ∧ (B ≈ D ∧ D ⊆ A)) → A ≈ D)
69		ensymi 6037	. . 3 ⊢ (B ≈ D → D ≈ B)
70	69	ad2antrl 708	. 2 ⊢ (((A ≈ C ∧ C ⊆ B) ∧ (B ≈ D ∧ D ⊆ A)) → D ≈ B)
71		entr 6039	. 2 ⊢ ((A ≈ D ∧ D ≈ B) → A ≈ B)
72	68, 70, 71	syl2anc 642	1 ⊢ (((A ≈ C ∧ C ⊆ B) ∧ (B ≈ D ∧ D ⊆ A)) → A ≈ B)

This proof depends on syntax axioms:   → wi 4   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2860   ⊆ wss 3258   class class class wbr 4640   ∘ 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 proof depends on 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 proof 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 used by:  sbth  6207