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 14385

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 13978	. . . . . . . 8 ⊢ (1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin
2		ficardom 9912	. . . . . . . 8 ⊢ ((1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin → (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω)
3	1, 2	ax-mp 5	. . . . . . 7 ⊢ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω
4		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
5	4	hashgval 14339	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
6	5	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
7	4	hashgval 14339	. . . . . . . . . . . . . 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 14362	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ₀)
10	9	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ∈ ℕ₀)
11		hashcl 14362	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
12	11	ad2antlr 737	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ₀)
13		simpr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))
14		nn0sub2 12627	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀)
15	10, 12, 13, 14	syl3anc 1389	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀)
16		hashfz1 14352	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐵) − (♯‘𝐴)) ∈ ℕ₀ → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴)))
17	15, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴)))
18	8, 17	eqtrid 2808	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = ((♯‘𝐵) − (♯‘𝐴)))
19	6, 18	oveq12d 7408	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))))
20	9	nn0cnd 12537	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℂ)
21	11	nn0cnd 12537	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℂ)
22		pncan3 11431	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) ∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
23	20, 21, 22	syl2an 605	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
24	23	adantr 484	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴))) = (♯‘𝐵))
25	19, 24	eqtrd 2796	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = (♯‘𝐵))
26		ficardom 9912	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
27	26	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (card‘𝐴) ∈ ω)
28	4	hashgadd 14383	. . . . . . . . . . 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 595	. . . . . . . . . 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 14339	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
31	30	ad2antlr 737	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
32	25, 29, 31	3eqtr4d 2806	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)))
33	32	fveq2d 6865	. . . . . . . 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 13977	. . . . . . . . 9 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ₀
35		nnacl 8574	. . . . . . . . . 10 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω)
36	27, 3, 35	sylancl 595	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω)
37		f1ocnvfv1 7254	. . . . . . . . 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 596	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))) = ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))
39		ficardom 9912	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → (card‘𝐵) ∈ ω)
40	39	ad2antlr 737	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (card‘𝐵) ∈ ω)
41		f1ocnvfv1 7254	. . . . . . . . 9 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ₀ ∧ (card‘𝐵) ∈ ω) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵))
42	34, 40, 41	sylancr 596	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (^◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵))
43	33, 38, 42	3eqtr3d 2804	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵))
44		oveq2 7398	. . . . . . . . 9 ⊢ (𝑦 = (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → ((card‘𝐴) +_o 𝑦) = ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))))
45	44	eqeq1d 2763	. . . . . . . 8 ⊢ (𝑦 = (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → (((card‘𝐴) +_o 𝑦) = (card‘𝐵) ↔ ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)))
46	45	rspcev 3580	. . . . . . 7 ⊢ (((card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω ∧ ((card‘𝐴) +_o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵))
47	3, 43, 46	sylancr 596	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵))
48	47	ex 416	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) → ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
49		cardnn 9914	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (card‘𝑦) = 𝑦)
50	49	adantl 485	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (card‘𝑦) = 𝑦)
51	50	oveq2d 7406	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → ((card‘𝐴) +_o (card‘𝑦)) = ((card‘𝐴) +_o 𝑦))
52	51	eqeq1d 2763	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) ↔ ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
53		fveq2 6861	. . . . . . . 8 ⊢ (((card‘𝐴) +_o (card‘𝑦)) = (card‘𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)))
54		nnfi 9129	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → 𝑦 ∈ Fin)
55		ficardom 9912	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → (card‘𝑦) ∈ ω)
56	4	hashgadd 14383	. . . . . . . . . . . . . 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 605	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦))))
58	4	hashgval 14339	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦)) = (♯‘𝑦))
59	5, 58	oveqan12d 7409	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
60	57, 59	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
61	60	adantlr 725	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦)))
62	30	ad2antlr 737	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵))
63	61, 62	eqeq12d 2777	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) ↔ ((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵)))
64		hashcl 14362	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
65	64	nn0ge0d 12538	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → 0 ≤ (♯‘𝑦))
66	65	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → 0 ≤ (♯‘𝑦))
67	9	nn0red 12536	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℝ)
68	64	nn0red 12536	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℝ)
69		addge01 11690	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐴) ∈ ℝ ∧ (♯‘𝑦) ∈ ℝ) → (0 ≤ (♯‘𝑦) ↔ (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦))))
70	67, 68, 69	syl2an 605	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (0 ≤ (♯‘𝑦) ↔ (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦))))
71	66, 70	mpbid 234	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)))
72	71	adantlr 725	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)))
73		breq2 5101	. . . . . . . . . . 11 ⊢ (((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵) → ((♯‘𝐴) ≤ ((♯‘𝐴) + (♯‘𝑦)) ↔ (♯‘𝐴) ≤ (♯‘𝐵)))
74	72, 73	syl5ibcom 247	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
75	63, 74	sylbid 242	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((card‘𝐴) +_o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵)))
76	54, 75	sylan2 602	. . . . . . . 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 262	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) → (((card‘𝐴) +_o 𝑦) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
79	78	rexlimdva 3162	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵)))
80	48, 79	impbid 214	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
81		nnawordex 8600	. . . . 5 ⊢ (((card‘𝐴) ∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
82	26, 39, 81	syl2an 605	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω ((card‘𝐴) +_o 𝑦) = (card‘𝐵)))
83		finnum 9899	. . . . 5 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)
84		finnum 9899	. . . . 5 ⊢ (𝐵 ∈ Fin → 𝐵 ∈ dom card)
85		carddom2 9928	. . . . 5 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))
86	83, 84, 85	syl2an 605	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))
87	80, 82, 86	3bitr2d 309	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
88	87	adantlr 725	. 2 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
89		hashxrcl 14363	. . . . . 6 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℝ^*)
90	89	ad2antrr 736	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ∈ ℝ^*)
91		pnfge 13125	. . . . 5 ⊢ ((♯‘𝐴) ∈ ℝ^* → (♯‘𝐴) ≤ +∞)
92	90, 91	syl 17	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ +∞)
93		hashinf 14341	. . . . 5 ⊢ ((𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
94	93	adantll 724	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
95	92, 94	breqtrrd 5125	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ (♯‘𝐵))
96		isinffi 9943	. . . . . 6 ⊢ ((¬ 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
97	96	ancoms 462	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
98	97	adantlr 725	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵)
99		brdomg 8932	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
100	99	ad2antlr 737	. . . 4 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
101	98, 100	mpbird 259	. . 3 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → 𝐴 ≼ 𝐵)
102	95, 101	2thd 267	. 2 ⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
103	88, 102	pm2.61dan 822	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1559 ∃wex 1798 ∈ wcel 2141 ∃wrex 3085 Vcvv 3453 ⊆ wss 3902 class class class wbr 5097 ↦ cmpt 5178 ^◡ccnv 5642 dom cdm 5643 ↾ cres 5645 –1-1→wf1 6512 –1-1-onto→wf1o 6514 ‘cfv 6515 (class class class)co 7390 ωcom 7840 reccrdg 8373 +_o coa 8427 ≼ cdom 8918 Fincfn 8920 cardccrd 9886 ℂcc 11064 ℝcr 11065 0cc0 11066 1c1 11067 + caddc 11069 +∞cpnf 11206 ℝ^*cxr 11208 ≤ cle 11210 − cmin 11407 ℕ₀cn0 12474 ...cfz 13505 ♯chash 14336

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-cnex 11122 ax-resscn 11123 ax-1cn 11124 ax-icn 11125 ax-addcl 11126 ax-addrcl 11127 ax-mulcl 11128 ax-mulrcl 11129 ax-mulcom 11130 ax-addass 11131 ax-mulass 11132 ax-distr 11133 ax-i2m1 11134 ax-1ne0 11135 ax-1rid 11136 ax-rnegex 11137 ax-rrecex 11138 ax-cnre 11139 ax-pre-lttri 11140 ax-pre-lttrn 11141 ax-pre-ltadd 11142 ax-pre-mulgt0 11143

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-1st 7964 df-2nd 7965 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-oadd 8434 df-er 8671 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-card 9890 df-pnf 11211 df-mnf 11212 df-xr 11213 df-ltxr 11214 df-le 11215 df-sub 11409 df-neg 11410 df-nn 12204 df-n0 12475 df-xnn0 12548 df-z 12562 df-uz 12833 df-fz 13506 df-hash 14337

This theorem is referenced by: hashdomi 14386 hashsdom 14387 hashun2 14389 hashss 14415 hashsslei 14432 hashfun 14443 hashf1 14463 hashge3el3dif 14493 isercoll 15685 phicl2 16793 phibnd 16796 prmreclem2 16943 prmreclem3 16944 4sqlem11 16981 vdwlem11 17017 ramub2 17040 0ram 17046 ram0 17048 sylow1lem4 19631 pgpssslw 19644 fislw 19655 znfld 21599 znidomb 21600 fta1blem 26218 birthdaylem3 27005 basellem4 27135 ppiwordi 27213 musum 27242 ppiub 27255 chpub 27271 lgsqrlem4 27400 upgrex 29249 sizusglecusg 29620 derangenlem 35481 subfaclefac 35486 erdsze2lem1 35513 snmlff 35639 hashnexinj 42705 idomsubgmo 43730 aacllem 50382

W3C validator