erdszelem8

	Ref	Expression
Hypotheses	erdsze.n	$⊢ φ \to N \in ℕ$
	erdsze.f	$⊢ φ \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
	erdszelem.k	$⊢ K = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\}] ℝ <))$
	erdszelem.o	$⊢ O Or ℝ$
	erdszelem.a	$⊢ φ \to A \in (1 \dots N)$
	erdszelem.b	$⊢ φ \to B \in (1 \dots N)$
	erdszelem.l	$⊢ φ \to A < B$
Assertion	erdszelem8	$⊢ φ \to (K (A) = K (B) \to \neg F (A) O F (B))$

Proof

Step	Hyp	Ref	Expression
1		erdsze.n	$⊢ φ \to N \in ℕ$
2		erdsze.f	$⊢ φ \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
3		erdszelem.k	$⊢ K = (x \in (1 \dots N) ⟼ sup (\|.\| [\{y \in 𝒫 (1 \dots x) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land x \in y)\}] ℝ <))$
4		erdszelem.o	$⊢ O Or ℝ$
5		erdszelem.a	$⊢ φ \to A \in (1 \dots N)$
6		erdszelem.b	$⊢ φ \to B \in (1 \dots N)$
7		erdszelem.l	$⊢ φ \to A < B$
8		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
9		ffun	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to Fun \|.\|$
10	8 9	ax-mp	$⊢ Fun \|.\|$
11	1 2 3 4	erdszelem5	$⊢ (φ \land A \in (1 \dots N)) \to K (A) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$
12	5 11	mpdan	$⊢ φ \to K (A) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]$
13		fvelima	$⊢ (Fun \|.\| \land K (A) \in \|.\| [\{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}]) \to \exists f \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \|f\| = K (A)$
14	10 12 13	sylancr	$⊢ φ \to \exists f \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \|f\| = K (A)$
15		eqid	$⊢ \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} = \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}$
16	15	erdszelem1	$⊢ f \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \leftrightarrow (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)$
17		fzfid	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to (1 \dots A) \in Fin$
18		simplr1	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to f \subseteq (1 \dots A)$
19		ssfi	$⊢ ((1 \dots A) \in Fin \land f \subseteq (1 \dots A)) \to f \in Fin$
20	17 18 19	syl2anc	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to f \in Fin$
21		hashcl	$⊢ f \in Fin \to \|f\| \in ℕ_{0}$
22	20 21	syl	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|f\| \in ℕ_{0}$
23	22	nn0red	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|f\| \in ℝ$
24		eqid	$⊢ \{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\} = \{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}$
25	24	erdszelem2	$⊢ (\|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \in Fin \land \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \subseteq ℕ)$
26	25	simpri	$⊢ \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \subseteq ℕ$
27		nnssre	$⊢ ℕ \subseteq ℝ$
28	26 27	sstri	$⊢ \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \subseteq ℝ$
29	28	a1i	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \subseteq ℝ$
30	5	elfzelzd	$⊢ φ \to A \in ℤ$
31	6	elfzelzd	$⊢ φ \to B \in ℤ$
32		elfznn	$⊢ A \in (1 \dots N) \to A \in ℕ$
33	5 32	syl	$⊢ φ \to A \in ℕ$
34	33	nnred	$⊢ φ \to A \in ℝ$
35		elfznn	$⊢ B \in (1 \dots N) \to B \in ℕ$
36	6 35	syl	$⊢ φ \to B \in ℕ$
37	36	nnred	$⊢ φ \to B \in ℝ$
38	34 37 7	ltled	$⊢ φ \to A \leq B$
39		eluz2	$⊢ B \in ℤ_{\geq A} \leftrightarrow (A \in ℤ \land B \in ℤ \land A \leq B)$
40	30 31 38 39	syl3anbrc	$⊢ φ \to B \in ℤ_{\geq A}$
41		fzss2	$⊢ B \in ℤ_{\geq A} \to (1 \dots A) \subseteq (1 \dots B)$
42	40 41	syl	$⊢ φ \to (1 \dots A) \subseteq (1 \dots B)$
43	42	ad2antrr	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to (1 \dots A) \subseteq (1 \dots B)$
44	18 43	sstrd	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to f \subseteq (1 \dots B)$
45		elfz1end	$⊢ B \in ℕ \leftrightarrow B \in (1 \dots B)$
46	36 45	sylib	$⊢ φ \to B \in (1 \dots B)$
47	46	ad2antrr	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to B \in (1 \dots B)$
48	47	snssd	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \{B\} \subseteq (1 \dots B)$
49	44 48	unssd	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to f \cup \{B\} \subseteq (1 \dots B)$
50		simplr2	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to ({F ↾}_{f}) {Isom}_{<, O} (f, F [f])$
51		f1f	$⊢ F : (1 \dots N) \underset{1-1}{⟶} ℝ \to F : (1 \dots N) ⟶ ℝ$
52	2 51	syl	$⊢ φ \to F : (1 \dots N) ⟶ ℝ$
53	52	ad2antrr	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to F : (1 \dots N) ⟶ ℝ$
54		elfzuz3	$⊢ A \in (1 \dots N) \to N \in ℤ_{\geq A}$
55		fzss2	$⊢ N \in ℤ_{\geq A} \to (1 \dots A) \subseteq (1 \dots N)$
56	5 54 55	3syl	$⊢ φ \to (1 \dots A) \subseteq (1 \dots N)$
57	56	ad2antrr	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to (1 \dots A) \subseteq (1 \dots N)$
58	18 57	sstrd	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to f \subseteq (1 \dots N)$
59		fzssuz	$⊢ (1 \dots N) \subseteq ℤ_{\geq 1}$
60		uzssz	$⊢ ℤ_{\geq 1} \subseteq ℤ$
61		zssre	$⊢ ℤ \subseteq ℝ$
62	60 61	sstri	$⊢ ℤ_{\geq 1} \subseteq ℝ$
63	59 62	sstri	$⊢ (1 \dots N) \subseteq ℝ$
64		ltso	$⊢ < Or ℝ$
65		soss	$⊢ (1 \dots N) \subseteq ℝ \to (< Or ℝ \to < Or (1 \dots N))$
66	63 64 65	mp2	$⊢ < Or (1 \dots N)$
67		soisores	$⊢ ((< Or (1 \dots N) \land O Or ℝ) \land (F : (1 \dots N) ⟶ ℝ \land f \subseteq (1 \dots N))) \to (({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \leftrightarrow \forall z \in f \forall w \in f (z < w \to F (z) O F (w)))$
68	66 4 67	mpanl12	$⊢ (F : (1 \dots N) ⟶ ℝ \land f \subseteq (1 \dots N)) \to (({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \leftrightarrow \forall z \in f \forall w \in f (z < w \to F (z) O F (w)))$
69	53 58 68	syl2anc	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to (({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \leftrightarrow \forall z \in f \forall w \in f (z < w \to F (z) O F (w)))$
70	50 69	mpbid	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \forall z \in f \forall w \in f (z < w \to F (z) O F (w))$
71	70	r19.21bi	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to \forall w \in f (z < w \to F (z) O F (w))$
72	18	sselda	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to z \in (1 \dots A)$
73		elfzle2	$⊢ z \in (1 \dots A) \to z \leq A$
74	72 73	syl	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to z \leq A$
75	58	sselda	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to z \in (1 \dots N)$
76	63 75	sselid	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to z \in ℝ$
77	5	ad3antrrr	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to A \in (1 \dots N)$
78	77 32	syl	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to A \in ℕ$
79	78	nnred	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to A \in ℝ$
80	76 79	lenltd	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to (z \leq A \leftrightarrow \neg A < z)$
81	74 80	mpbid	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to \neg A < z$
82	50	adantr	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to ({F ↾}_{f}) {Isom}_{<, O} (f, F [f])$
83		simplr3	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to A \in f$
84	83	adantr	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to A \in f$
85		simpr	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to z \in f$
86		isorel	$⊢ (({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land (A \in f \land z \in f)) \to (A < z \leftrightarrow ({F ↾}_{f}) (A) O ({F ↾}_{f}) (z))$
87		fvres	$⊢ A \in f \to ({F ↾}_{f}) (A) = F (A)$
88		fvres	$⊢ z \in f \to ({F ↾}_{f}) (z) = F (z)$
89	87 88	breqan12d	$⊢ (A \in f \land z \in f) \to (({F ↾}_{f}) (A) O ({F ↾}_{f}) (z) \leftrightarrow F (A) O F (z))$
90	89	adantl	$⊢ (({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land (A \in f \land z \in f)) \to (({F ↾}_{f}) (A) O ({F ↾}_{f}) (z) \leftrightarrow F (A) O F (z))$
91	86 90	bitrd	$⊢ (({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land (A \in f \land z \in f)) \to (A < z \leftrightarrow F (A) O F (z))$
92	82 84 85 91	syl12anc	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to (A < z \leftrightarrow F (A) O F (z))$
93	81 92	mtbid	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to \neg F (A) O F (z)$
94		simplr	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to F (A) O F (B)$
95	53	adantr	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to F : (1 \dots N) ⟶ ℝ$
96	95 75	ffvelrnd	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to F (z) \in ℝ$
97	95 77	ffvelrnd	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to F (A) \in ℝ$
98	6	ad2antrr	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to B \in (1 \dots N)$
99	98	adantr	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to B \in (1 \dots N)$
100	95 99	ffvelrnd	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to F (B) \in ℝ$
101		sotr2	$⊢ (O Or ℝ \land (F (z) \in ℝ \land F (A) \in ℝ \land F (B) \in ℝ)) \to ((\neg F (A) O F (z) \land F (A) O F (B)) \to F (z) O F (B))$
102	4 101	mpan	$⊢ (F (z) \in ℝ \land F (A) \in ℝ \land F (B) \in ℝ) \to ((\neg F (A) O F (z) \land F (A) O F (B)) \to F (z) O F (B))$
103	96 97 100 102	syl3anc	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to ((\neg F (A) O F (z) \land F (A) O F (B)) \to F (z) O F (B))$
104	93 94 103	mp2and	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to F (z) O F (B)$
105	104	a1d	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to (z < w \to F (z) O F (B))$
106		elsni	$⊢ w \in \{B\} \to w = B$
107	106	fveq2d	$⊢ w \in \{B\} \to F (w) = F (B)$
108	107	breq2d	$⊢ w \in \{B\} \to (F (z) O F (w) \leftrightarrow F (z) O F (B))$
109	108	imbi2d	$⊢ w \in \{B\} \to ((z < w \to F (z) O F (w)) \leftrightarrow (z < w \to F (z) O F (B)))$
110	105 109	syl5ibrcom	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to (w \in \{B\} \to (z < w \to F (z) O F (w)))$
111	110	ralrimiv	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to \forall w \in \{B\} (z < w \to F (z) O F (w))$
112		ralunb	$⊢ \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w)) \leftrightarrow (\forall w \in f (z < w \to F (z) O F (w)) \land \forall w \in \{B\} (z < w \to F (z) O F (w)))$
113	71 111 112	sylanbrc	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land z \in f) \to \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w))$
114	113	ralrimiva	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \forall z \in f \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w))$
115	49	sselda	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land w \in (f \cup \{B\})) \to w \in (1 \dots B)$
116		elfzle2	$⊢ w \in (1 \dots B) \to w \leq B$
117	116	adantl	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land w \in (1 \dots B)) \to w \leq B$
118		elfzelz	$⊢ w \in (1 \dots B) \to w \in ℤ$
119	118	zred	$⊢ w \in (1 \dots B) \to w \in ℝ$
120	119	adantl	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land w \in (1 \dots B)) \to w \in ℝ$
121	37	ad3antrrr	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land w \in (1 \dots B)) \to B \in ℝ$
122	120 121	lenltd	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land w \in (1 \dots B)) \to (w \leq B \leftrightarrow \neg B < w)$
123	117 122	mpbid	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land w \in (1 \dots B)) \to \neg B < w$
124	115 123	syldan	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land w \in (f \cup \{B\})) \to \neg B < w$
125	124	pm2.21d	$⊢ (((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \land w \in (f \cup \{B\})) \to (B < w \to F (z) O F (w))$
126	125	ralrimiva	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \forall w \in (f \cup \{B\}) (B < w \to F (z) O F (w))$
127		elsni	$⊢ z \in \{B\} \to z = B$
128	127	breq1d	$⊢ z \in \{B\} \to (z < w \leftrightarrow B < w)$
129	128	imbi1d	$⊢ z \in \{B\} \to ((z < w \to F (z) O F (w)) \leftrightarrow (B < w \to F (z) O F (w)))$
130	129	ralbidv	$⊢ z \in \{B\} \to (\forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w)) \leftrightarrow \forall w \in (f \cup \{B\}) (B < w \to F (z) O F (w)))$
131	126 130	syl5ibrcom	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to (z \in \{B\} \to \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w)))$
132	131	ralrimiv	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \forall z \in \{B\} \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w))$
133		ralunb	$⊢ \forall z \in (f \cup \{B\}) \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w)) \leftrightarrow (\forall z \in f \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w)) \land \forall z \in \{B\} \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w)))$
134	114 132 133	sylanbrc	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \forall z \in (f \cup \{B\}) \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w))$
135	98	snssd	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \{B\} \subseteq (1 \dots N)$
136	58 135	unssd	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to f \cup \{B\} \subseteq (1 \dots N)$
137		soisores	$⊢ ((< Or (1 \dots N) \land O Or ℝ) \land (F : (1 \dots N) ⟶ ℝ \land f \cup \{B\} \subseteq (1 \dots N))) \to (({F ↾}_{(f \cup \{B\})}) {Isom}_{<, O} (f \cup \{B\}, F [f \cup \{B\}]) \leftrightarrow \forall z \in (f \cup \{B\}) \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w)))$
138	66 4 137	mpanl12	$⊢ (F : (1 \dots N) ⟶ ℝ \land f \cup \{B\} \subseteq (1 \dots N)) \to (({F ↾}_{(f \cup \{B\})}) {Isom}_{<, O} (f \cup \{B\}, F [f \cup \{B\}]) \leftrightarrow \forall z \in (f \cup \{B\}) \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w)))$
139	53 136 138	syl2anc	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to (({F ↾}_{(f \cup \{B\})}) {Isom}_{<, O} (f \cup \{B\}, F [f \cup \{B\}]) \leftrightarrow \forall z \in (f \cup \{B\}) \forall w \in (f \cup \{B\}) (z < w \to F (z) O F (w)))$
140	134 139	mpbird	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to ({F ↾}_{(f \cup \{B\})}) {Isom}_{<, O} (f \cup \{B\}, F [f \cup \{B\}])$
141		ssun2	$⊢ \{B\} \subseteq f \cup \{B\}$
142		snssg	$⊢ B \in (1 \dots B) \to (B \in (f \cup \{B\}) \leftrightarrow \{B\} \subseteq f \cup \{B\})$
143	47 142	syl	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to (B \in (f \cup \{B\}) \leftrightarrow \{B\} \subseteq f \cup \{B\})$
144	141 143	mpbiri	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to B \in (f \cup \{B\})$
145	24	erdszelem1	$⊢ f \cup \{B\} \in \{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\} \leftrightarrow (f \cup \{B\} \subseteq (1 \dots B) \land ({F ↾}_{(f \cup \{B\})}) {Isom}_{<, O} (f \cup \{B\}, F [f \cup \{B\}]) \land B \in (f \cup \{B\}))$
146	49 140 144 145	syl3anbrc	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to f \cup \{B\} \in \{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}$
147		vex	$⊢ f \in V$
148		snex	$⊢ \{B\} \in V$
149	147 148	unex	$⊢ f \cup \{B\} \in V$
150	8	fdmi	$⊢ dom \|.\| = V$
151	149 150	eleqtrri	$⊢ f \cup \{B\} \in dom \|.\|$
152		funfvima	$⊢ (Fun \|.\| \land f \cup \{B\} \in dom \|.\|) \to (f \cup \{B\} \in \{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\} \to \|f \cup \{B\}\| \in \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}])$
153	10 151 152	mp2an	$⊢ f \cup \{B\} \in \{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\} \to \|f \cup \{B\}\| \in \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}]$
154	146 153	syl	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|f \cup \{B\}\| \in \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}]$
155	154	ne0d	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \neq \emptyset$
156	25	simpli	$⊢ \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \in Fin$
157		fimaxre2	$⊢ (\|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \subseteq ℝ \land \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \in Fin) \to \exists z \in ℝ \forall w \in \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] w \leq z$
158	29 156 157	sylancl	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \exists z \in ℝ \forall w \in \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] w \leq z$
159	34 37	ltnled	$⊢ φ \to (A < B \leftrightarrow \neg B \leq A)$
160	7 159	mpbid	$⊢ φ \to \neg B \leq A$
161		elfzle2	$⊢ B \in (1 \dots A) \to B \leq A$
162	160 161	nsyl	$⊢ φ \to \neg B \in (1 \dots A)$
163	162	ad2antrr	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \neg B \in (1 \dots A)$
164	18 163	ssneldd	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \neg B \in f$
165		hashunsng	$⊢ B \in (1 \dots N) \to ((f \in Fin \land \neg B \in f) \to \|f \cup \{B\}\| = \|f\| + 1)$
166	98 165	syl	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to ((f \in Fin \land \neg B \in f) \to \|f \cup \{B\}\| = \|f\| + 1)$
167	20 164 166	mp2and	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|f \cup \{B\}\| = \|f\| + 1$
168	167 154	eqeltrrd	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|f\| + 1 \in \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}]$
169		suprub	$⊢ ((\|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \subseteq ℝ \land \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \neq \emptyset \land \exists z \in ℝ \forall w \in \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] w \leq z) \land \|f\| + 1 \in \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}]) \to \|f\| + 1 \leq sup (\|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] ℝ <)$
170	29 155 158 168 169	syl31anc	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|f\| + 1 \leq sup (\|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] ℝ <)$
171	1 2 3	erdszelem3	$⊢ B \in (1 \dots N) \to K (B) = sup (\|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] ℝ <)$
172	6 171	syl	$⊢ φ \to K (B) = sup (\|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] ℝ <)$
173	172	ad2antrr	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to K (B) = sup (\|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] ℝ <)$
174	170 173	breqtrrd	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|f\| + 1 \leq K (B)$
175	1 2 3 4	erdszelem6	$⊢ φ \to K : (1 \dots N) ⟶ ℕ$
176	175 6	ffvelrnd	$⊢ φ \to K (B) \in ℕ$
177	176	ad2antrr	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to K (B) \in ℕ$
178	177	nnnn0d	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to K (B) \in ℕ_{0}$
179		nn0ltp1le	$⊢ (\|f\| \in ℕ_{0} \land K (B) \in ℕ_{0}) \to (\|f\| < K (B) \leftrightarrow \|f\| + 1 \leq K (B))$
180	22 178 179	syl2anc	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to (\|f\| < K (B) \leftrightarrow \|f\| + 1 \leq K (B))$
181	174 180	mpbird	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|f\| < K (B)$
182	23 181	ltned	$⊢ ((φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \land F (A) O F (B)) \to \|f\| \neq K (B)$
183	182	ex	$⊢ (φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \to (F (A) O F (B) \to \|f\| \neq K (B))$
184		neeq1	$⊢ \|f\| = K (A) \to (\|f\| \neq K (B) \leftrightarrow K (A) \neq K (B))$
185	184	imbi2d	$⊢ \|f\| = K (A) \to ((F (A) O F (B) \to \|f\| \neq K (B)) \leftrightarrow (F (A) O F (B) \to K (A) \neq K (B)))$
186	183 185	syl5ibcom	$⊢ (φ \land (f \subseteq (1 \dots A) \land ({F ↾}_{f}) {Isom}_{<, O} (f, F [f]) \land A \in f)) \to (\|f\| = K (A) \to (F (A) O F (B) \to K (A) \neq K (B)))$
187	16 186	sylan2b	$⊢ (φ \land f \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\}) \to (\|f\| = K (A) \to (F (A) O F (B) \to K (A) \neq K (B)))$
188	187	rexlimdva	$⊢ φ \to (\exists f \in \{y \in 𝒫 (1 \dots A) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land A \in y)\} \|f\| = K (A) \to (F (A) O F (B) \to K (A) \neq K (B)))$
189	14 188	mpd	$⊢ φ \to (F (A) O F (B) \to K (A) \neq K (B))$
190	189	necon2bd	$⊢ φ \to (K (A) = K (B) \to \neg F (A) O F (B))$

Metamath Proof Explorer

Theorem erdszelem8

Proof