erdszelem9

	Ref	Expression
Hypotheses	erdsze.n	$⊢ φ \to N \in ℕ$
	erdsze.f	$⊢ φ \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
	erdszelem.i	$⊢ I = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, <} (y, F [y]) \land x \in y)\}] ℝ <))$
	erdszelem.j	$⊢ J = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, <^{-1}} (y, F [y]) \land x \in y)\}] ℝ <))$
	erdszelem.t	$⊢ T = (n \in (1 \dots N) ⟼ ⟨I (n), J (n)⟩)$
Assertion	erdszelem9	$⊢ φ \to T : (1 \dots N) \underset{1-1}{⟶} ℕ \times ℕ$

Proof

Step	Hyp	Ref	Expression
1		erdsze.n	$⊢ φ \to N \in ℕ$
2		erdsze.f	$⊢ φ \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
3		erdszelem.i	$⊢ I = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, <} (y, F [y]) \land x \in y)\}] ℝ <))$
4		erdszelem.j	$⊢ J = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, <^{-1}} (y, F [y]) \land x \in y)\}] ℝ <))$
5		erdszelem.t	$⊢ T = (n \in (1 \dots N) ⟼ ⟨I (n), J (n)⟩)$
6		ltso	$⊢ < Or ℝ$
7	1 2 3 6	erdszelem6	$⊢ φ \to I : (1 \dots N) ⟶ ℕ$
8	7	ffvelrnda	$⊢ (φ \land n \in (1 \dots N)) \to I (n) \in ℕ$
9		gtso	$⊢ <^{-1} Or ℝ$
10	1 2 4 9	erdszelem6	$⊢ φ \to J : (1 \dots N) ⟶ ℕ$
11	10	ffvelrnda	$⊢ (φ \land n \in (1 \dots N)) \to J (n) \in ℕ$
12		opelxpi	$⊢ (I (n) \in ℕ \land J (n) \in ℕ) \to ⟨I (n), J (n)⟩ \in (ℕ \times ℕ)$
13	8 11 12	syl2anc	$⊢ (φ \land n \in (1 \dots N)) \to ⟨I (n), J (n)⟩ \in (ℕ \times ℕ)$
14	13 5	fmptd	$⊢ φ \to T : (1 \dots N) ⟶ ℕ \times ℕ$
15		fveq2	$⊢ a = z \to T (a) = T (z)$
16		fveq2	$⊢ b = w \to T (b) = T (w)$
17	15 16	eqeqan12d	$⊢ (a = z \land b = w) \to (T (a) = T (b) \leftrightarrow T (z) = T (w))$
18		eqeq12	$⊢ (a = z \land b = w) \to (a = b \leftrightarrow z = w)$
19	17 18	imbi12d	$⊢ (a = z \land b = w) \to ((T (a) = T (b) \to a = b) \leftrightarrow (T (z) = T (w) \to z = w))$
20		fveq2	$⊢ a = w \to T (a) = T (w)$
21		fveq2	$⊢ b = z \to T (b) = T (z)$
22	20 21	eqeqan12d	$⊢ (a = w \land b = z) \to (T (a) = T (b) \leftrightarrow T (w) = T (z))$
23		eqcom	$⊢ T (w) = T (z) \leftrightarrow T (z) = T (w)$
24	22 23	bitrdi	$⊢ (a = w \land b = z) \to (T (a) = T (b) \leftrightarrow T (z) = T (w))$
25		eqeq12	$⊢ (a = w \land b = z) \to (a = b \leftrightarrow w = z)$
26		eqcom	$⊢ w = z \leftrightarrow z = w$
27	25 26	bitrdi	$⊢ (a = w \land b = z) \to (a = b \leftrightarrow z = w)$
28	24 27	imbi12d	$⊢ (a = w \land b = z) \to ((T (a) = T (b) \to a = b) \leftrightarrow (T (z) = T (w) \to z = w))$
29		elfzelz	$⊢ z \in (1 \dots N) \to z \in ℤ$
30	29	zred	$⊢ z \in (1 \dots N) \to z \in ℝ$
31	30	ssriv	$⊢ (1 \dots N) \subseteq ℝ$
32	31	a1i	$⊢ φ \to (1 \dots N) \subseteq ℝ$
33		biidd	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N))) \to ((T (z) = T (w) \to z = w) \leftrightarrow (T (z) = T (w) \to z = w))$
34		simpr1	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to z \in (1 \dots N)$
35		fveq2	$⊢ n = z \to I (n) = I (z)$
36		fveq2	$⊢ n = z \to J (n) = J (z)$
37	35 36	opeq12d	$⊢ n = z \to ⟨I (n), J (n)⟩ = ⟨I (z), J (z)⟩$
38		opex	$⊢ ⟨I (z), J (z)⟩ \in V$
39	37 5 38	fvmpt	$⊢ z \in (1 \dots N) \to T (z) = ⟨I (z), J (z)⟩$
40	34 39	syl	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to T (z) = ⟨I (z), J (z)⟩$
41		simpr2	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to w \in (1 \dots N)$
42		fveq2	$⊢ n = w \to I (n) = I (w)$
43		fveq2	$⊢ n = w \to J (n) = J (w)$
44	42 43	opeq12d	$⊢ n = w \to ⟨I (n), J (n)⟩ = ⟨I (w), J (w)⟩$
45		opex	$⊢ ⟨I (w), J (w)⟩ \in V$
46	44 5 45	fvmpt	$⊢ w \in (1 \dots N) \to T (w) = ⟨I (w), J (w)⟩$
47	41 46	syl	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to T (w) = ⟨I (w), J (w)⟩$
48	40 47	eqeq12d	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (T (z) = T (w) \leftrightarrow ⟨I (z), J (z)⟩ = ⟨I (w), J (w)⟩)$
49		fvex	$⊢ I (z) \in V$
50		fvex	$⊢ J (z) \in V$
51	49 50	opth	$⊢ ⟨I (z), J (z)⟩ = ⟨I (w), J (w)⟩ \leftrightarrow (I (z) = I (w) \land J (z) = J (w))$
52	34 30	syl	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to z \in ℝ$
53	31 41	sselid	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to w \in ℝ$
54		simpr3	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to z \leq w$
55	52 53 54	leltned	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (z < w \leftrightarrow w \neq z)$
56	2	adantr	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
57		f1fveq	$⊢ (F : (1 \dots N) \underset{1-1}{⟶} ℝ \land (z \in (1 \dots N) \land w \in (1 \dots N))) \to (F (z) = F (w) \leftrightarrow z = w)$
58	56 34 41 57	syl12anc	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (F (z) = F (w) \leftrightarrow z = w)$
59	58 26	bitr4di	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (F (z) = F (w) \leftrightarrow w = z)$
60	59	necon3bid	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (F (z) \neq F (w) \leftrightarrow w \neq z)$
61	55 60	bitr4d	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (z < w \leftrightarrow F (z) \neq F (w))$
62	61	biimpa	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to F (z) \neq F (w)$
63		f1f	$⊢ F : (1 \dots N) \underset{1-1}{⟶} ℝ \to F : (1 \dots N) ⟶ ℝ$
64	2 63	syl	$⊢ φ \to F : (1 \dots N) ⟶ ℝ$
65	64	ad2antrr	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to F : (1 \dots N) ⟶ ℝ$
66	34	adantr	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to z \in (1 \dots N)$
67	65 66	ffvelrnd	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to F (z) \in ℝ$
68	41	adantr	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to w \in (1 \dots N)$
69	65 68	ffvelrnd	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to F (w) \in ℝ$
70	67 69	lttri2d	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to (F (z) \neq F (w) \leftrightarrow (F (z) < F (w) \lor F (w) < F (z)))$
71	62 70	mpbid	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to (F (z) < F (w) \lor F (w) < F (z))$
72	1	ad2antrr	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to N \in ℕ$
73	2	ad2antrr	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
74		simpr	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to z < w$
75	72 73 3 6 66 68 74	erdszelem8	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to (I (z) = I (w) \to \neg F (z) < F (w))$
76	72 73 4 9 66 68 74	erdszelem8	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to (J (z) = J (w) \to \neg F (z) <^{-1} F (w))$
77	75 76	anim12d	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to ((I (z) = I (w) \land J (z) = J (w)) \to (\neg F (z) < F (w) \land \neg F (z) <^{-1} F (w)))$
78		ioran	$⊢ \neg (F (z) < F (w) \lor F (w) < F (z)) \leftrightarrow (\neg F (z) < F (w) \land \neg F (w) < F (z))$
79		fvex	$⊢ F (z) \in V$
80		fvex	$⊢ F (w) \in V$
81	79 80	brcnv	$⊢ F (z) <^{-1} F (w) \leftrightarrow F (w) < F (z)$
82	81	notbii	$⊢ \neg F (z) <^{-1} F (w) \leftrightarrow \neg F (w) < F (z)$
83	82	anbi2i	$⊢ (\neg F (z) < F (w) \land \neg F (z) <^{-1} F (w)) \leftrightarrow (\neg F (z) < F (w) \land \neg F (w) < F (z))$
84	78 83	bitr4i	$⊢ \neg (F (z) < F (w) \lor F (w) < F (z)) \leftrightarrow (\neg F (z) < F (w) \land \neg F (z) <^{-1} F (w))$
85	77 84	syl6ibr	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to ((I (z) = I (w) \land J (z) = J (w)) \to \neg (F (z) < F (w) \lor F (w) < F (z)))$
86	71 85	mt2d	$⊢ ((φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \land z < w) \to \neg (I (z) = I (w) \land J (z) = J (w))$
87	86	ex	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (z < w \to \neg (I (z) = I (w) \land J (z) = J (w)))$
88	55 87	sylbird	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (w \neq z \to \neg (I (z) = I (w) \land J (z) = J (w)))$
89	88	necon4ad	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to ((I (z) = I (w) \land J (z) = J (w)) \to w = z)$
90	51 89	syl5bi	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (⟨I (z), J (z)⟩ = ⟨I (w), J (w)⟩ \to w = z)$
91	48 90	sylbid	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (T (z) = T (w) \to w = z)$
92	91 26	syl6ib	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N) \land z \leq w)) \to (T (z) = T (w) \to z = w)$
93	19 28 32 33 92	wlogle	$⊢ (φ \land (z \in (1 \dots N) \land w \in (1 \dots N))) \to (T (z) = T (w) \to z = w)$
94	93	ralrimivva	$⊢ φ \to \forall z \in (1 \dots N) \forall w \in (1 \dots N) (T (z) = T (w) \to z = w)$
95		dff13	$⊢ T : (1 \dots N) \underset{1-1}{⟶} ℕ \times ℕ \leftrightarrow (T : (1 \dots N) ⟶ ℕ \times ℕ \land \forall z \in (1 \dots N) \forall w \in (1 \dots N) (T (z) = T (w) \to z = w))$
96	14 94 95	sylanbrc	$⊢ φ \to T : (1 \dots N) \underset{1-1}{⟶} ℕ \times ℕ$

Metamath Proof Explorer

Theorem erdszelem9

Proof