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 14417

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 14010	. . . . . . . 8 ⊢ (1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin
2		ficardom 9948	. . . . . . . 8 ⊢ ((1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin → (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω)
3	1, 2	ax-mp 5	. . . . . . 7 ⊢ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω
4		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
5	4	hashgval 14371	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
6	5	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
7	4	hashgval 14371	. . . . . . . . . . . . . 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 14394	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
10	9	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ∈ ℕ₀)
11		hashcl 14394	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
12	11	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ₀)
13		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))
14		nn0sub2 12658	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀)
15	10, 12, 13, 14	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀)
16		hashfz1 14384	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀ → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴)))
17	15, 16	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴)))
18	8, 17	eqtrid 2810	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = ((♯‘𝐵) − (♯‘𝐴)))
19	6, 18	oveq12d 7430	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))))
20	9	nn0cnd 12568	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℂ)
21	11	nn0cnd 12568	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℂ)
22		pncan3 11466	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) ∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
23	20, 21, 22	syl2an 607	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
24	23	adantr 485	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
25	19, 24	eqtrd 2798	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = (♯‘𝐵))
26		ficardom 9948	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
27	26	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (card‘𝐴) ∈ ω)
28	4	hashgadd 14415	. . . . . . . . . . 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 597	. . . . . . . . . 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 14371	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
31	30	ad2antlr 739	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
32	25, 29, 31	3eqtr4d 2808	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)))
33	32	fveq2d 6887	. . . . . . . 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 14009	. . . . . . . . 9 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ₀
35		nnacl 8598	. . . . . . . . . 10 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω)
36	27, 3, 35	sylancl 597	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω)
37		f1ocnvfv1 7276	. . . . . . . . 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 598	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))) = ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))
39		ficardom 9948	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → (card‘𝐵) ∈ ω)
40	39	ad2antlr 739	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (card‘𝐵) ∈ ω)
41		f1ocnvfv1 7276	. . . . . . . . 9 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ₀ ∧ (card‘𝐵) ∈ ω) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵))
42	34, 40, 41	sylancr 598	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵))
43	33, 38, 42	3eqtr3d 2806	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵))
44		oveq2 7420	. . . . . . . . 9 ⊢ (𝑦 = (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → ((card‘𝐴) +_o 𝑦) = ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))
45	44	eqeq1d 2765	. . . . . . . 8 ⊢ (𝑦 = (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → (((card‘𝐴) +_o 𝑦) = (card‘𝐵) ↔ ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)))
46	45	rspcev 3582	. . . . . . 7 ⊢ (((card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω ∧ ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵))
47	3, 43, 46	sylancr 598	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵))
48	47	ex 417	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
49		cardnn 9950	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (card‘𝑦) = 𝑦)
50	49	adantl 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (card‘𝑦) = 𝑦)
51	50	oveq2d 7428	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → ((card‘𝐴) +_o (card‘𝑦)) = ((card‘𝐴) +_o 𝑦))
52	51	eqeq1d 2765	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) ↔ ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
53		fveq2 6883	. . . . . . . 8 ⊢ (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)))
54		nnfi 9153	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → 𝑦 ∈ Fin)
55		ficardom 9948	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → (card‘𝑦) ∈ ω)
56	4	hashgadd 14415	. . . . . . . . . . . . . 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 607	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦))))
58	4	hashgval 14371	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦)) = (♯‘𝑦))
59	5, 58	oveqan12d 7431	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
60	57, 59	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
61	60	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
62	30	ad2antlr 739	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
63	61, 62	eqeq12d 2779	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) ↔ ((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵)))
64		hashcl 14394	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
65	64	nn0ge0d 12569	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → 0 ≤ (♯‘𝑦))
66	65	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → 0 ≤ (♯‘𝑦))
67	9	nn0red 12567	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℝ)
68	64	nn0red 12567	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℝ)
69		addge01 11725	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐴) ∈ ℝ ∧ (♯‘𝑦) ∈ ℝ) → (0 ≤ (♯‘𝑦) ↔ (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦))))
70	67, 68, 69	syl2an 607	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (0 ≤ (♯‘𝑦) ↔ (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦))))
71	66, 70	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)))
72	71	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)))
73		breq2 5114	. . . . . . . . . . 11 ⊢ (((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵) → ((♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)) ↔ (♯‘𝐴) ≤ (♯‘𝐵)))
74	72, 73	syl5ibcom 248	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
75	63, 74	sylbid 243	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵)))
76	54, 75	sylan2 604	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵)))
77	53, 76	syl5 35	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
78	52, 77	sylbird 263	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((card‘𝐴) +_o 𝑦) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
79	78	rexlimdva 3166	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
80	48, 79	impbid 215	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
81		nnawordex 8624	. . . . 5 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
82	26, 39, 81	syl2an 607	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
83		finnum 9935	. . . . 5 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)
84		finnum 9935	. . . . 5 ⊢ (𝐵 ∈ Fin → 𝐵 ∈ dom card)
85		carddom2 9964	. . . . 5 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))
86	83, 84, 85	syl2an 607	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))
87	80, 82, 86	3bitr2d 310	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
88	87	adantlr 727	. 2 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
89		hashxrcl 14395	. . . . . 6 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℝ^*)
90	89	ad2antrr 738	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ∈ ℝ^*)
91		pnfge 13156	. . . . 5 ⊢ ((♯‘𝐴) ∈ ℝ^* → (♯‘𝐴) ≤ +∞)
92	90, 91	syl 18	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ +∞)
93		hashinf 14373	. . . . 5 ⊢ ((𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
94	93	adantll 726	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
95	92, 94	breqtrrd 5140	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ (♯‘𝐵))
96		isinffi 9979	. . . . . 6 ⊢ ((¬ 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
97	96	ancoms 463	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
98	97	adantlr 727	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
99		brdomg 8956	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
100	99	ad2antlr 739	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
101	98, 100	mpbird 260	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → 𝐴 ≼ 𝐵)
102	95, 101	2thd 268	. 2 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
103	88, 102	pm2.61dan 824	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∃wex 1809 ∈ wcel 2143 ∃wrex 3089 Vcvv 3455 ⊆ wss 3906 class class class wbr 5110 ↦ cmpt 5193 ^◡ccnv 5662 dom cdm 5663 ↾ cres 5665 –1-1→wf1 6535 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7412 ωcom 7863 reccrdg 8397 +_o coa 8451 ≼ cdom 8942 Fincfn 8944 cardccrd 9922 ℂcc 11099 ℝcr 11100 0cc0 11101 1c1 11102 + caddc 11104 +∞cpnf 11241 ℝ^*cxr 11243 ≤ cle 11245 − cmin 11442 ℕ₀cn0 12505 ...cfz 13536 ♯chash 14368

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-oadd 8458 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-card 9926 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-nn 12235 df-n0 12506 df-xnn0 12579 df-z 12593 df-uz 12864 df-fz 13537 df-hash 14369

This theorem is referenced by: hashdomi 14418 hashsdom 14419 hashun2 14421 hashss 14447 hashsslei 14465 hashfun 14476 hashf1 14496 hashge3el3dif 14526 isercoll 15721 phicl2 16828 phibnd 16831 prmreclem2 16978 prmreclem3 16979 4sqlem11 17016 vdwlem11 17052 ramub2 17075 0ram 17081 ram0 17083 sylow1lem4 19672 pgpssslw 19685 fislw 19696 znfld 21691 znidomb 21692 fta1blem 26309 birthdaylem3 27099 basellem4 27229 ppiwordi 27307 musum 27336 ppiub 27349 chpub 27365 lgsqrlem4 27494 upgrex 29423 sizusglecusg 29794 derangenlem 35644 subfaclefac 35649 erdsze2lem1 35676 snmlff 35802 hashnexinj 42876 idomsubgmo 43903 aacllem 50584

W3C validator