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 14341

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 13934	. . . . . . . 8 ⊢ (1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin
2		ficardom 9885	. . . . . . . 8 ⊢ ((1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin → (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω)
3	1, 2	ax-mp 5	. . . . . . 7 ⊢ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω
4		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
5	4	hashgval 14295	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
6	5	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
7	4	hashgval 14295	. . . . . . . . . . . . . 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 14318	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
10	9	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ∈ ℕ₀)
11		hashcl 14318	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
12	11	ad2antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ₀)
13		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))
14		nn0sub2 12590	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀)
15	10, 12, 13, 14	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀)
16		hashfz1 14308	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀ → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴)))
17	15, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴)))
18	8, 17	eqtrid 2783	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = ((♯‘𝐵) − (♯‘𝐴)))
19	6, 18	oveq12d 7385	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))))
20	9	nn0cnd 12500	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℂ)
21	11	nn0cnd 12500	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℂ)
22		pncan3 11401	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) ∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
23	20, 21, 22	syl2an 597	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
24	23	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
25	19, 24	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = (♯‘𝐵))
26		ficardom 9885	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
27	26	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (card‘𝐴) ∈ ω)
28	4	hashgadd 14339	. . . . . . . . . . 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 587	. . . . . . . . . 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 14295	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
31	30	ad2antlr 728	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
32	25, 29, 31	3eqtr4d 2781	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)))
33	32	fveq2d 6844	. . . . . . . 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 13933	. . . . . . . . 9 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ₀
35		nnacl 8547	. . . . . . . . . 10 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω)
36	27, 3, 35	sylancl 587	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω)
37		f1ocnvfv1 7231	. . . . . . . . 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 588	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))) = ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))
39		ficardom 9885	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → (card‘𝐵) ∈ ω)
40	39	ad2antlr 728	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (card‘𝐵) ∈ ω)
41		f1ocnvfv1 7231	. . . . . . . . 9 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ₀ ∧ (card‘𝐵) ∈ ω) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵))
42	34, 40, 41	sylancr 588	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵))
43	33, 38, 42	3eqtr3d 2779	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵))
44		oveq2 7375	. . . . . . . . 9 ⊢ (𝑦 = (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → ((card‘𝐴) +_o 𝑦) = ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))
45	44	eqeq1d 2738	. . . . . . . 8 ⊢ (𝑦 = (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → (((card‘𝐴) +_o 𝑦) = (card‘𝐵) ↔ ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)))
46	45	rspcev 3564	. . . . . . 7 ⊢ (((card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω ∧ ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵))
47	3, 43, 46	sylancr 588	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵))
48	47	ex 412	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
49		cardnn 9887	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (card‘𝑦) = 𝑦)
50	49	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (card‘𝑦) = 𝑦)
51	50	oveq2d 7383	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → ((card‘𝐴) +_o (card‘𝑦)) = ((card‘𝐴) +_o 𝑦))
52	51	eqeq1d 2738	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) ↔ ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
53		fveq2 6840	. . . . . . . 8 ⊢ (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)))
54		nnfi 9102	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → 𝑦 ∈ Fin)
55		ficardom 9885	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → (card‘𝑦) ∈ ω)
56	4	hashgadd 14339	. . . . . . . . . . . . . 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 597	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦))))
58	4	hashgval 14295	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦)) = (♯‘𝑦))
59	5, 58	oveqan12d 7386	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
60	57, 59	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
61	60	adantlr 716	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
62	30	ad2antlr 728	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
63	61, 62	eqeq12d 2752	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) ↔ ((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵)))
64		hashcl 14318	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
65	64	nn0ge0d 12501	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → 0 ≤ (♯‘𝑦))
66	65	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → 0 ≤ (♯‘𝑦))
67	9	nn0red 12499	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℝ)
68	64	nn0red 12499	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℝ)
69		addge01 11660	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐴) ∈ ℝ ∧ (♯‘𝑦) ∈ ℝ) → (0 ≤ (♯‘𝑦) ↔ (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦))))
70	67, 68, 69	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (0 ≤ (♯‘𝑦) ↔ (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦))))
71	66, 70	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)))
72	71	adantlr 716	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)))
73		breq2 5089	. . . . . . . . . . 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 594	. . . . . . . 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 3138	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
80	48, 79	impbid 212	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
81		nnawordex 8573	. . . . 5 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
82	26, 39, 81	syl2an 597	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
83		finnum 9872	. . . . 5 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)
84		finnum 9872	. . . . 5 ⊢ (𝐵 ∈ Fin → 𝐵 ∈ dom card)
85		carddom2 9901	. . . . 5 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))
86	83, 84, 85	syl2an 597	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))
87	80, 82, 86	3bitr2d 307	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
88	87	adantlr 716	. 2 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
89		hashxrcl 14319	. . . . . 6 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℝ^*)
90	89	ad2antrr 727	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ∈ ℝ^*)
91		pnfge 13081	. . . . 5 ⊢ ((♯‘𝐴) ∈ ℝ^* → (♯‘𝐴) ≤ +∞)
92	90, 91	syl 17	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ +∞)
93		hashinf 14297	. . . . 5 ⊢ ((𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
94	93	adantll 715	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
95	92, 94	breqtrrd 5113	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ (♯‘𝐵))
96		isinffi 9916	. . . . . 6 ⊢ ((¬ 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
97	96	ancoms 458	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
98	97	adantlr 716	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
99		brdomg 8905	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
100	99	ad2antlr 728	. . . 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 813	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ∃wrex 3061 Vcvv 3429 ⊆ wss 3889 class class class wbr 5085 ↦ cmpt 5166 ^◡ccnv 5630 dom cdm 5631 ↾ cres 5633 –1-1→wf1 6495 –1-1-onto→wf1o 6497 ‘cfv 6498 (class class class)co 7367 ωcom 7817 reccrdg 8348 +_o coa 8402 ≼ cdom 8891 Fincfn 8893 cardccrd 9859 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 +∞cpnf 11176 ℝ^*cxr 11178 ≤ cle 11180 − cmin 11377 ℕ₀cn0 12437 ...cfz 13461 ♯chash 14292

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-oadd 8409 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-n0 12438 df-xnn0 12511 df-z 12525 df-uz 12789 df-fz 13462 df-hash 14293

This theorem is referenced by: hashdomi 14342 hashsdom 14343 hashun2 14345 hashss 14371 hashsslei 14388 hashfun 14399 hashf1 14419 hashge3el3dif 14449 isercoll 15630 phicl2 16738 phibnd 16741 prmreclem2 16888 prmreclem3 16889 4sqlem11 16926 vdwlem11 16962 ramub2 16985 0ram 16991 ram0 16993 sylow1lem4 19576 pgpssslw 19589 fislw 19600 znfld 21540 znidomb 21541 fta1blem 26136 birthdaylem3 26917 basellem4 27047 ppiwordi 27125 musum 27154 ppiub 27167 chpub 27183 lgsqrlem4 27312 upgrex 29161 sizusglecusg 29532 derangenlem 35353 subfaclefac 35358 erdsze2lem1 35385 snmlff 35511 hashnexinj 42567 idomsubgmo 43621 aacllem 50276

W3C validator