erdsze2lem1

	Ref	Expression
Hypotheses	erdsze2.r	$⊢ φ \to R \in ℕ$
	erdsze2.s	$⊢ φ \to S \in ℕ$
	erdsze2.f	$⊢ φ \to F : A \underset{1-1}{⟶} ℝ$
	erdsze2.a	$⊢ φ \to A \subseteq ℝ$
	erdsze2lem.n	$⊢ N = (R - 1) (S - 1)$
	erdsze2lem.l	$⊢ φ \to N < \|A\|$
Assertion	erdsze2lem1	$⊢ φ \to \exists f (f : (1 \dots N + 1) \underset{1-1}{⟶} A \land f {Isom}_{<, <} ((1 \dots N + 1), ran f))$

Proof

Step	Hyp	Ref	Expression
1		erdsze2.r	$⊢ φ \to R \in ℕ$
2		erdsze2.s	$⊢ φ \to S \in ℕ$
3		erdsze2.f	$⊢ φ \to F : A \underset{1-1}{⟶} ℝ$
4		erdsze2.a	$⊢ φ \to A \subseteq ℝ$
5		erdsze2lem.n	$⊢ N = (R - 1) (S - 1)$
6		erdsze2lem.l	$⊢ φ \to N < \|A\|$
7		nnm1nn0	$⊢ R \in ℕ \to R - 1 \in ℕ_{0}$
8	1 7	syl	$⊢ φ \to R - 1 \in ℕ_{0}$
9		nnm1nn0	$⊢ S \in ℕ \to S - 1 \in ℕ_{0}$
10	2 9	syl	$⊢ φ \to S - 1 \in ℕ_{0}$
11	8 10	nn0mulcld	$⊢ φ \to (R - 1) (S - 1) \in ℕ_{0}$
12	5 11	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
13		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
14		hashfz1	$⊢ N + 1 \in ℕ_{0} \to \|(1 \dots N + 1)\| = N + 1$
15	12 13 14	3syl	$⊢ φ \to \|(1 \dots N + 1)\| = N + 1$
16	15	adantr	$⊢ (φ \land A \in Fin) \to \|(1 \dots N + 1)\| = N + 1$
17	6	adantr	$⊢ (φ \land A \in Fin) \to N < \|A\|$
18		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
19		nn0ltp1le	$⊢ (N \in ℕ_{0} \land \|A\| \in ℕ_{0}) \to (N < \|A\| \leftrightarrow N + 1 \leq \|A\|)$
20	12 18 19	syl2an	$⊢ (φ \land A \in Fin) \to (N < \|A\| \leftrightarrow N + 1 \leq \|A\|)$
21	17 20	mpbid	$⊢ (φ \land A \in Fin) \to N + 1 \leq \|A\|$
22	16 21	eqbrtrd	$⊢ (φ \land A \in Fin) \to \|(1 \dots N + 1)\| \leq \|A\|$
23		fzfid	$⊢ (φ \land A \in Fin) \to (1 \dots N + 1) \in Fin$
24		simpr	$⊢ (φ \land A \in Fin) \to A \in Fin$
25		hashdom	$⊢ ((1 \dots N + 1) \in Fin \land A \in Fin) \to (\|(1 \dots N + 1)\| \leq \|A\| \leftrightarrow (1 \dots N + 1) ≼ A)$
26	23 24 25	syl2anc	$⊢ (φ \land A \in Fin) \to (\|(1 \dots N + 1)\| \leq \|A\| \leftrightarrow (1 \dots N + 1) ≼ A)$
27	22 26	mpbid	$⊢ (φ \land A \in Fin) \to (1 \dots N + 1) ≼ A$
28		simpr	$⊢ (φ \land \neg A \in Fin) \to \neg A \in Fin$
29		fzfid	$⊢ (φ \land \neg A \in Fin) \to (1 \dots N + 1) \in Fin$
30		isinffi	$⊢ (\neg A \in Fin \land (1 \dots N + 1) \in Fin) \to \exists f f : (1 \dots N + 1) \underset{1-1}{⟶} A$
31	28 29 30	syl2anc	$⊢ (φ \land \neg A \in Fin) \to \exists f f : (1 \dots N + 1) \underset{1-1}{⟶} A$
32		reex	$⊢ ℝ \in V$
33		ssexg	$⊢ (A \subseteq ℝ \land ℝ \in V) \to A \in V$
34	4 32 33	sylancl	$⊢ φ \to A \in V$
35	34	adantr	$⊢ (φ \land \neg A \in Fin) \to A \in V$
36		brdomg	$⊢ A \in V \to ((1 \dots N + 1) ≼ A \leftrightarrow \exists f f : (1 \dots N + 1) \underset{1-1}{⟶} A)$
37	35 36	syl	$⊢ (φ \land \neg A \in Fin) \to ((1 \dots N + 1) ≼ A \leftrightarrow \exists f f : (1 \dots N + 1) \underset{1-1}{⟶} A)$
38	31 37	mpbird	$⊢ (φ \land \neg A \in Fin) \to (1 \dots N + 1) ≼ A$
39	27 38	pm2.61dan	$⊢ φ \to (1 \dots N + 1) ≼ A$
40		domeng	$⊢ A \in V \to ((1 \dots N + 1) ≼ A \leftrightarrow \exists s ((1 \dots N + 1) \approx s \land s \subseteq A))$
41	34 40	syl	$⊢ φ \to ((1 \dots N + 1) ≼ A \leftrightarrow \exists s ((1 \dots N + 1) \approx s \land s \subseteq A))$
42	39 41	mpbid	$⊢ φ \to \exists s ((1 \dots N + 1) \approx s \land s \subseteq A)$
43		simprr	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to s \subseteq A$
44	4	adantr	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to A \subseteq ℝ$
45	43 44	sstrd	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to s \subseteq ℝ$
46		ltso	$⊢ < Or ℝ$
47		soss	$⊢ s \subseteq ℝ \to (< Or ℝ \to < Or s)$
48	45 46 47	mpisyl	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to < Or s$
49		fzfid	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to (1 \dots N + 1) \in Fin$
50		simprl	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to (1 \dots N + 1) \approx s$
51		enfi	$⊢ (1 \dots N + 1) \approx s \to ((1 \dots N + 1) \in Fin \leftrightarrow s \in Fin)$
52	50 51	syl	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to ((1 \dots N + 1) \in Fin \leftrightarrow s \in Fin)$
53	49 52	mpbid	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to s \in Fin$
54		fz1iso	$⊢ (< Or s \land s \in Fin) \to \exists f f {Isom}_{<, <} ((1 \dots \|s\|), s)$
55	48 53 54	syl2anc	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to \exists f f {Isom}_{<, <} ((1 \dots \|s\|), s)$
56		isof1o	$⊢ f {Isom}_{<, <} ((1 \dots \|s\|), s) \to f : (1 \dots \|s\|) \underset{1-1 onto}{⟶} s$
57	56	adantl	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to f : (1 \dots \|s\|) \underset{1-1 onto}{⟶} s$
58		hashen	$⊢ ((1 \dots N + 1) \in Fin \land s \in Fin) \to (\|(1 \dots N + 1)\| = \|s\| \leftrightarrow (1 \dots N + 1) \approx s)$
59	49 53 58	syl2anc	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to (\|(1 \dots N + 1)\| = \|s\| \leftrightarrow (1 \dots N + 1) \approx s)$
60	50 59	mpbird	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to \|(1 \dots N + 1)\| = \|s\|$
61	15	adantr	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to \|(1 \dots N + 1)\| = N + 1$
62	60 61	eqtr3d	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to \|s\| = N + 1$
63	62	adantr	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to \|s\| = N + 1$
64	63	oveq2d	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to (1 \dots \|s\|) = (1 \dots N + 1)$
65	64	f1oeq2d	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to (f : (1 \dots \|s\|) \underset{1-1 onto}{⟶} s \leftrightarrow f : (1 \dots N + 1) \underset{1-1 onto}{⟶} s)$
66	57 65	mpbid	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to f : (1 \dots N + 1) \underset{1-1 onto}{⟶} s$
67		f1of1	$⊢ f : (1 \dots N + 1) \underset{1-1 onto}{⟶} s \to f : (1 \dots N + 1) \underset{1-1}{⟶} s$
68	66 67	syl	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to f : (1 \dots N + 1) \underset{1-1}{⟶} s$
69		simplrr	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to s \subseteq A$
70		f1ss	$⊢ (f : (1 \dots N + 1) \underset{1-1}{⟶} s \land s \subseteq A) \to f : (1 \dots N + 1) \underset{1-1}{⟶} A$
71	68 69 70	syl2anc	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to f : (1 \dots N + 1) \underset{1-1}{⟶} A$
72		simpr	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to f {Isom}_{<, <} ((1 \dots \|s\|), s)$
73		f1ofo	$⊢ f : (1 \dots \|s\|) \underset{1-1 onto}{⟶} s \to f : (1 \dots \|s\|) \underset{onto}{⟶} s$
74		forn	$⊢ f : (1 \dots \|s\|) \underset{onto}{⟶} s \to ran f = s$
75		isoeq5	$⊢ ran f = s \to (f {Isom}_{<, <} ((1 \dots \|s\|), ran f) \leftrightarrow f {Isom}_{<, <} ((1 \dots \|s\|), s))$
76	57 73 74 75	4syl	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to (f {Isom}_{<, <} ((1 \dots \|s\|), ran f) \leftrightarrow f {Isom}_{<, <} ((1 \dots \|s\|), s))$
77	72 76	mpbird	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to f {Isom}_{<, <} ((1 \dots \|s\|), ran f)$
78		isoeq4	$⊢ (1 \dots \|s\|) = (1 \dots N + 1) \to (f {Isom}_{<, <} ((1 \dots \|s\|), ran f) \leftrightarrow f {Isom}_{<, <} ((1 \dots N + 1), ran f))$
79	64 78	syl	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to (f {Isom}_{<, <} ((1 \dots \|s\|), ran f) \leftrightarrow f {Isom}_{<, <} ((1 \dots N + 1), ran f))$
80	77 79	mpbid	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to f {Isom}_{<, <} ((1 \dots N + 1), ran f)$
81	71 80	jca	$⊢ ((φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \land f {Isom}_{<, <} ((1 \dots \|s\|), s)) \to (f : (1 \dots N + 1) \underset{1-1}{⟶} A \land f {Isom}_{<, <} ((1 \dots N + 1), ran f))$
82	81	ex	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to (f {Isom}_{<, <} ((1 \dots \|s\|), s) \to (f : (1 \dots N + 1) \underset{1-1}{⟶} A \land f {Isom}_{<, <} ((1 \dots N + 1), ran f)))$
83	82	eximdv	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to (\exists f f {Isom}_{<, <} ((1 \dots \|s\|), s) \to \exists f (f : (1 \dots N + 1) \underset{1-1}{⟶} A \land f {Isom}_{<, <} ((1 \dots N + 1), ran f)))$
84	55 83	mpd	$⊢ (φ \land ((1 \dots N + 1) \approx s \land s \subseteq A)) \to \exists f (f : (1 \dots N + 1) \underset{1-1}{⟶} A \land f {Isom}_{<, <} ((1 \dots N + 1), ran f))$
85	42 84	exlimddv	$⊢ φ \to \exists f (f : (1 \dots N + 1) \underset{1-1}{⟶} A \land f {Isom}_{<, <} ((1 \dots N + 1), ran f))$

Metamath Proof Explorer

Theorem erdsze2lem1

Proof