hashdom - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hashdom		Structured version Visualization version GIF version

Theorem hashdom 14344

Description: Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 22-Apr-2015.)

**Assertion**
Ref	Expression
hashdom	⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))

Proof of Theorem hashdom Dummy variables 𝑥 𝑓 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfi 13937	. . . . . . . 8 ⊢ (1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin
2		ficardom 9914	. . . . . . . 8 ⊢ ((1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin → (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω)
3	1, 2	ax-mp 5	. . . . . . 7 ⊢ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω
4		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
5	4	hashgval 14298	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
6	5	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
7	4	hashgval 14298	. . . . . . . . . . . . . 14 ⊢ ((1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))))
8	1, 7	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (♯‘(1...((♯‘𝐵) − (♯‘𝐴))))
9		hashcl 14321	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
10	9	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ∈ ℕ₀)
11		hashcl 14321	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
12	11	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ₀)
13		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))
14		nn0sub2 12595	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀)
15	10, 12, 13, 14	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀)
16		hashfz1 14311	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀ → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴)))
17	15, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴)))
18	8, 17	eqtrid 2776	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = ((♯‘𝐵) − (♯‘𝐴)))
19	6, 18	oveq12d 7405	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))))
20	9	nn0cnd 12505	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℂ)
21	11	nn0cnd 12505	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℂ)
22		pncan3 11429	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) ∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
23	20, 21, 22	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
24	23	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
25	19, 24	eqtrd 2764	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = (♯‘𝐵))
26		ficardom 9914	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
27	26	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (card‘𝐴) ∈ ω)
28	4	hashgadd 14342	. . . . . . . . . . 11 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))))
29	27, 3, 28	sylancl 586	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))))
30	4	hashgval 14298	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
31	30	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
32	25, 29, 31	3eqtr4d 2774	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)))
33	32	fveq2d 6862	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))) = (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))))
34	4	hashgf1o 13936	. . . . . . . . 9 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ₀
35		nnacl 8575	. . . . . . . . . 10 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω)
36	27, 3, 35	sylancl 586	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω)
37		f1ocnvfv1 7251	. . . . . . . . 9 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ₀ ∧ ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))) = ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))
38	34, 36, 37	sylancr 587	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))) = ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))
39		ficardom 9914	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → (card‘𝐵) ∈ ω)
40	39	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (card‘𝐵) ∈ ω)
41		f1ocnvfv1 7251	. . . . . . . . 9 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ₀ ∧ (card‘𝐵) ∈ ω) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵))
42	34, 40, 41	sylancr 587	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵))
43	33, 38, 42	3eqtr3d 2772	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵))
44		oveq2 7395	. . . . . . . . 9 ⊢ (𝑦 = (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → ((card‘𝐴) +_o 𝑦) = ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))
45	44	eqeq1d 2731	. . . . . . . 8 ⊢ (𝑦 = (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → (((card‘𝐴) +_o 𝑦) = (card‘𝐵) ↔ ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)))
46	45	rspcev 3588	. . . . . . 7 ⊢ (((card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω ∧ ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵))
47	3, 43, 46	sylancr 587	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵))
48	47	ex 412	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
49		cardnn 9916	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (card‘𝑦) = 𝑦)
50	49	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (card‘𝑦) = 𝑦)
51	50	oveq2d 7403	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → ((card‘𝐴) +_o (card‘𝑦)) = ((card‘𝐴) +_o 𝑦))
52	51	eqeq1d 2731	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) ↔ ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
53		fveq2 6858	. . . . . . . 8 ⊢ (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)))
54		nnfi 9131	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → 𝑦 ∈ Fin)
55		ficardom 9914	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → (card‘𝑦) ∈ ω)
56	4	hashgadd 14342	. . . . . . . . . . . . . 14 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘𝑦) ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦))))
57	26, 55, 56	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦))))
58	4	hashgval 14298	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦)) = (♯‘𝑦))
59	5, 58	oveqan12d 7406	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
60	57, 59	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
61	60	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
62	30	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
63	61, 62	eqeq12d 2745	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) ↔ ((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵)))
64		hashcl 14321	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
65	64	nn0ge0d 12506	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → 0 ≤ (♯‘𝑦))
66	65	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → 0 ≤ (♯‘𝑦))
67	9	nn0red 12504	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℝ)
68	64	nn0red 12504	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℝ)
69		addge01 11688	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐴) ∈ ℝ ∧ (♯‘𝑦) ∈ ℝ) → (0 ≤ (♯‘𝑦) ↔ (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦))))
70	67, 68, 69	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (0 ≤ (♯‘𝑦) ↔ (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦))))
71	66, 70	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)))
72	71	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)))
73		breq2 5111	. . . . . . . . . . 11 ⊢ (((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵) → ((♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)) ↔ (♯‘𝐴) ≤ (♯‘𝐵)))
74	72, 73	syl5ibcom 245	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
75	63, 74	sylbid 240	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵)))
76	54, 75	sylan2 593	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵)))
77	53, 76	syl5 34	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
78	52, 77	sylbird 260	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((card‘𝐴) +_o 𝑦) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
79	78	rexlimdva 3134	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
80	48, 79	impbid 212	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
81		nnawordex 8601	. . . . 5 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
82	26, 39, 81	syl2an 596	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
83		finnum 9901	. . . . 5 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)
84		finnum 9901	. . . . 5 ⊢ (𝐵 ∈ Fin → 𝐵 ∈ dom card)
85		carddom2 9930	. . . . 5 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))
86	83, 84, 85	syl2an 596	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))
87	80, 82, 86	3bitr2d 307	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
88	87	adantlr 715	. 2 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
89		hashxrcl 14322	. . . . . 6 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℝ^*)
90	89	ad2antrr 726	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ∈ ℝ^*)
91		pnfge 13090	. . . . 5 ⊢ ((♯‘𝐴) ∈ ℝ^* → (♯‘𝐴) ≤ +∞)
92	90, 91	syl 17	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ +∞)
93		hashinf 14300	. . . . 5 ⊢ ((𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
94	93	adantll 714	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
95	92, 94	breqtrrd 5135	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ (♯‘𝐵))
96		isinffi 9945	. . . . . 6 ⊢ ((¬ 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
97	96	ancoms 458	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
98	97	adantlr 715	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
99		brdomg 8930	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
100	99	ad2antlr 727	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
101	98, 100	mpbird 257	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → 𝐴 ≼ 𝐵)
102	95, 101	2thd 265	. 2 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
103	88, 102	pm2.61dan 812	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ∃wrex 3053 Vcvv 3447 ⊆ wss 3914 class class class wbr 5107 ↦ cmpt 5188 ^◡ccnv 5637 dom cdm 5638 ↾ cres 5640 –1-1→wf1 6508 –1-1-onto→wf1o 6510 ‘cfv 6511 (class class class)co 7387 ωcom 7842 reccrdg 8377 +_o coa 8431 ≼ cdom 8916 Fincfn 8918 cardccrd 9888 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 +∞cpnf 11205 ℝ^*cxr 11207 ≤ cle 11209 − cmin 11405 ℕ₀cn0 12442 ...cfz 13468 ♯chash 14295

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-oadd 8438 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-nn 12187 df-n0 12443 df-xnn0 12516 df-z 12530 df-uz 12794 df-fz 13469 df-hash 14296

This theorem is referenced by: hashdomi 14345 hashsdom 14346 hashun2 14348 hashss 14374 hashsslei 14391 hashfun 14402 hashf1 14422 hashge3el3dif 14452 isercoll 15634 phicl2 16738 phibnd 16741 prmreclem2 16888 prmreclem3 16889 4sqlem11 16926 vdwlem11 16962 ramub2 16985 0ram 16991 ram0 16993 sylow1lem4 19531 pgpssslw 19544 fislw 19555 znfld 21470 znidomb 21471 fta1blem 26076 birthdaylem3 26863 basellem4 26994 ppiwordi 27072 musum 27101 ppiub 27115 chpub 27131 lgsqrlem4 27260 upgrex 29019 sizusglecusg 29391 derangenlem 35158 subfaclefac 35163 erdsze2lem1 35190 snmlff 35316 hashnexinj 42116 idomsubgmo 43182 aacllem 49790

W3C validator