Theorem hasheqf1oi 14519

Description: The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 25-Dec-2017.) (Revised by AV, 4-May-2021.)

Assertion

Ref	Expression
hasheqf1oi	⊢ (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵)))

Distinct variable groups:   𝐴,𝑓   𝐵,𝑓   𝑓,𝑉

Proof of Theorem hasheqf1oi

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hasheqf1o 14517	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) = (♯‘𝐵) ↔ ∃𝑓 𝑓:𝐴⟶1-1onto𝐵))
2	1	biimprd 251	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵)))
3	2	a1d 26	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵))))
4		fiinfnf1o 14518	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ¬ ∃𝑓 𝑓:𝐴⟶1-1onto𝐵)
5	4	pm2.21d 122	. . 3 ⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵)))
6	5	a1d 26	. 2 ⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵))))
7		fiinfnf1o 14518	. . . 4 ⊢ ((𝐵 ∈ Fin ∧ ¬ 𝐴 ∈ Fin) → ¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴)
8		19.41v 1984	. . . . . . 7 ⊢ (∃𝑓(𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) ↔ (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉))
9		f1orel 6846	. . . . . . . . . . . . 13 ⊢ (𝑓:𝐴⟶1-1onto𝐵 → Rel 𝑓)
10	9	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → Rel 𝑓)
11		f1ocnvb 6857	. . . . . . . . . . . 12 ⊢ (Rel 𝑓 → (𝑓:𝐴⟶1-1onto𝐵 ↔ ◡𝑓:𝐵⟶1-1onto𝐴))
12	10, 11	syl 18	. . . . . . . . . . 11 ⊢ ((𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → (𝑓:𝐴⟶1-1onto𝐵 ↔ ◡𝑓:𝐵⟶1-1onto𝐴))
13		f1of 6843	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴⟶1-1onto𝐵 → 𝑓:𝐴⟶𝐵)
14		fex 7252	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝑓 ∈ V)
15	13, 14	sylan 592	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → 𝑓 ∈ V)
16		cnvexg 7957	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ V → ◡𝑓 ∈ V)
17		f1oeq1 6831	. . . . . . . . . . . . . 14 ⊢ (𝑔 = ◡𝑓 → (𝑔:𝐵⟶1-1onto𝐴 ↔ ◡𝑓:𝐵⟶1-1onto𝐴))
18	17	spcegv 3555	. . . . . . . . . . . . 13 ⊢ (◡𝑓 ∈ V → (◡𝑓:𝐵⟶1-1onto𝐴 → ∃𝑔 𝑔:𝐵⟶1-1onto𝐴))
19	15, 16, 18	3syl 19	. . . . . . . . . . . 12 ⊢ ((𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → (◡𝑓:𝐵⟶1-1onto𝐴 → ∃𝑔 𝑔:𝐵⟶1-1onto𝐴))
20		pm2.24 125	. . . . . . . . . . . 12 ⊢ (∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (♯‘𝐴) = (♯‘𝐵)))
21	19, 20	syl6 36	. . . . . . . . . . 11 ⊢ ((𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → (◡𝑓:𝐵⟶1-1onto𝐴 → (¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (♯‘𝐴) = (♯‘𝐵))))
22	12, 21	sylbid 243	. . . . . . . . . 10 ⊢ ((𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → (𝑓:𝐴⟶1-1onto𝐵 → (¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (♯‘𝐴) = (♯‘𝐵))))
23	22	com12 33	. . . . . . . . 9 ⊢ (𝑓:𝐴⟶1-1onto𝐵 → ((𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (♯‘𝐴) = (♯‘𝐵))))
24	23	anabsi5 682	. . . . . . . 8 ⊢ ((𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (♯‘𝐴) = (♯‘𝐵)))
25	24	exlimiv 1965	. . . . . . 7 ⊢ (∃𝑓(𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (♯‘𝐴) = (♯‘𝐵)))
26	8, 25	sylbir 238	. . . . . 6 ⊢ ((∃𝑓 𝑓:𝐴⟶1-1onto𝐵 ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (♯‘𝐴) = (♯‘𝐵)))
27	26	ex 418	. . . . 5 ⊢ (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (𝐴 ∈ 𝑉 → (¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (♯‘𝐴) = (♯‘𝐵))))
28	27	com13 89	. . . 4 ⊢ (¬ ∃𝑔 𝑔:𝐵⟶1-1onto𝐴 → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵))))
29	7, 28	syl 18	. . 3 ⊢ ((𝐵 ∈ Fin ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵))))
30	29	ancoms 464	. 2 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵))))
31		hashinf 14503	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞)
32	31	expcom 419	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ Fin → (𝐴 ∈ 𝑉 → (♯‘𝐴) = +∞))
33	32	adantr 486	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (♯‘𝐴) = +∞))
34	33	imp 412	. . . . . . 7 ⊢ (((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) → (♯‘𝐴) = +∞)
35	34	adantr 486	. . . . . 6 ⊢ ((((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴⟶1-1onto𝐵) → (♯‘𝐴) = +∞)
36		simpr 490	. . . . . . . 8 ⊢ (((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉)
37		f1ofo 6851	. . . . . . . 8 ⊢ (𝑓:𝐴⟶1-1onto𝐵 → 𝑓:𝐴⟶onto𝐵)
38		focdmex 7989	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → (𝑓:𝐴⟶onto𝐵 → 𝐵 ∈ V))
39	38	imp 412	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓:𝐴⟶onto𝐵) → 𝐵 ∈ V)
40	36, 37, 39	syl2an 608	. . . . . . 7 ⊢ ((((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴⟶1-1onto𝐵) → 𝐵 ∈ V)
41		hashinf 14503	. . . . . . . . 9 ⊢ ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
42	41	expcom 419	. . . . . . . 8 ⊢ (¬ 𝐵 ∈ Fin → (𝐵 ∈ V → (♯‘𝐵) = +∞))
43	42	ad3antlr 744	. . . . . . 7 ⊢ ((((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴⟶1-1onto𝐵) → (𝐵 ∈ V → (♯‘𝐵) = +∞))
44	40, 43	mpd 16	. . . . . 6 ⊢ ((((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴⟶1-1onto𝐵) → (♯‘𝐵) = +∞)
45	35, 44	eqtr4d 2801	. . . . 5 ⊢ ((((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝐴⟶1-1onto𝐵) → (♯‘𝐴) = (♯‘𝐵))
46	45	ex 418	. . . 4 ⊢ (((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) → (𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵)))
47	46	exlimdv 1968	. . 3 ⊢ (((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ∈ 𝑉) → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵)))
48	47	ex 418	. 2 ⊢ ((¬ 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵))))
49	3, 6, 30, 48	4cases 1056	1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴⟶1-1onto𝐵 → (♯‘𝐴) = (♯‘𝐵)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  Vcvv 3454  ^◡ccnv 5654  Rel wrel 5660  ⟶wf 6551  ⟶ontowfo 6553  ⟶1-1ontowf1o 6554  ‘cfv 6555  Fincfn 8998  +∞cpnf 11364  ♯chash 14498

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-nn 12360  df-n0 12631  df-z 12718  df-uz 12990  df-hash 14499

This theorem is used by:  hashf1rn  14520  hasheqf1od  14521  2lgslem1  27748  nbedgusgr  29980  rusgrnumwrdl2  30194  wwlksnexthasheq  30519  rusgrnumwlkg  30596  numclwwlkqhash  31003  bj-finsumval0  38397  aks6d1c2  43371