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		elfzelz	$⊢ A \in (1 \dots N) \to A \in ℤ$
31	5 30	syl	$⊢ φ \to A \in ℤ$
32		elfzelz	$⊢ B \in (1 \dots N) \to B \in ℤ$
33	6 32	syl	$⊢ φ \to B \in ℤ$
34		elfznn	$⊢ A \in (1 \dots N) \to A \in ℕ$
35	5 34	syl	$⊢ φ \to A \in ℕ$
36	35	nnred	$⊢ φ \to A \in ℝ$
37		elfznn	$⊢ B \in (1 \dots N) \to B \in ℕ$
38	6 37	syl	$⊢ φ \to B \in ℕ$
39	38	nnred	$⊢ φ \to B \in ℝ$
40	36 39 7	ltled	$⊢ φ \to A \leq B$
41		eluz2	$⊢ B \in ℤ_{\geq A} \leftrightarrow (A \in ℤ \land B \in ℤ \land A \leq B)$
42	31 33 40 41	syl3anbrc	$⊢ φ \to B \in ℤ_{\geq A}$
43		fzss2	$⊢ B \in ℤ_{\geq A} \to (1 \dots A) \subseteq (1 \dots B)$
44	42 43	syl	$⊢ φ \to (1 \dots A) \subseteq (1 \dots B)$
45	44	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)$
46	18 45	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)$
47		elfz1end	$⊢ B \in ℕ \leftrightarrow B \in (1 \dots B)$
48	38 47	sylib	$⊢ φ \to B \in (1 \dots B)$
49	48	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)$
50	49	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)$
51	46 50	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)$
52		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])$
53		f1f	$⊢ F : (1 \dots N) \underset{1-1}{⟶} ℝ \to F : (1 \dots N) ⟶ ℝ$
54	2 53	syl	$⊢ φ \to F : (1 \dots N) ⟶ ℝ$
55	54	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) ⟶ ℝ$
56		elfzuz3	$⊢ A \in (1 \dots N) \to N \in ℤ_{\geq A}$
57		fzss2	$⊢ N \in ℤ_{\geq A} \to (1 \dots A) \subseteq (1 \dots N)$
58	5 56 57	3syl	$⊢ φ \to (1 \dots A) \subseteq (1 \dots N)$
59	58	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)$
60	18 59	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)$
61		fzssuz	$⊢ (1 \dots N) \subseteq ℤ_{\geq 1}$
62		uzssz	$⊢ ℤ_{\geq 1} \subseteq ℤ$
63		zssre	$⊢ ℤ \subseteq ℝ$
64	62 63	sstri	$⊢ ℤ_{\geq 1} \subseteq ℝ$
65	61 64	sstri	$⊢ (1 \dots N) \subseteq ℝ$
66		ltso	$⊢ < Or ℝ$
67		soss	$⊢ (1 \dots N) \subseteq ℝ \to (< Or ℝ \to < Or (1 \dots N))$
68	65 66 67	mp2	$⊢ < Or (1 \dots N)$
69		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)))$
70	68 4 69	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)))$
71	55 60 70	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)))$
72	52 71	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))$
73	72	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))$
74	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)$
75		elfzle2	$⊢ z \in (1 \dots A) \to z \leq A$
76	74 75	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$
77	60	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)$
78	65 77	sseldi	$⊢ (((φ \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 ℝ$
79	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)$
80	79 34	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 ℕ$
81	80	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 ℝ$
82	78 81	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)$
83	76 82	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$
84	52	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])$
85		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$
86	85	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$
87		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$
88		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))$
89		fvres	$⊢ A \in f \to ({F ↾}_{f}) (A) = F (A)$
90		fvres	$⊢ z \in f \to ({F ↾}_{f}) (z) = F (z)$
91	89 90	breqan12d	$⊢ (A \in f \land z \in f) \to (({F ↾}_{f}) (A) O ({F ↾}_{f}) (z) \leftrightarrow F (A) O F (z))$
92	91	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))$
93	88 92	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))$
94	84 86 87 93	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))$
95	83 94	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)$
96		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)$
97	55	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) ⟶ ℝ$
98	97 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 (z) \in ℝ$
99	97 79	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 ℝ$
100	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)$
101	100	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)$
102	97 101	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 ℝ$
103		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))$
104	4 103	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))$
105	98 99 102 104	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))$
106	95 96 105	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)$
107	106	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))$
108		elsni	$⊢ w \in \{B\} \to w = B$
109	108	fveq2d	$⊢ w \in \{B\} \to F (w) = F (B)$
110	109	breq2d	$⊢ w \in \{B\} \to (F (z) O F (w) \leftrightarrow F (z) O F (B))$
111	110	imbi2d	$⊢ w \in \{B\} \to ((z < w \to F (z) O F (w)) \leftrightarrow (z < w \to F (z) O F (B)))$
112	107 111	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)))$
113	112	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))$
114		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)))$
115	73 113 114	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))$
116	115	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))$
117	51	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)$
118		elfzle2	$⊢ w \in (1 \dots B) \to w \leq B$
119	118	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$
120		elfzelz	$⊢ w \in (1 \dots B) \to w \in ℤ$
121	120	zred	$⊢ w \in (1 \dots B) \to w \in ℝ$
122	121	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 ℝ$
123	39	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 ℝ$
124	122 123	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)$
125	119 124	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$
126	117 125	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$
127	126	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))$
128	127	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))$
129		elsni	$⊢ z \in \{B\} \to z = B$
130	129	breq1d	$⊢ z \in \{B\} \to (z < w \leftrightarrow B < w)$
131	130	imbi1d	$⊢ z \in \{B\} \to ((z < w \to F (z) O F (w)) \leftrightarrow (B < w \to F (z) O F (w)))$
132	131	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)))$
133	128 132	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)))$
134	133	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))$
135		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)))$
136	116 134 135	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))$
137	100	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)$
138	60 137	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)$
139		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)))$
140	68 4 139	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)))$
141	55 138 140	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)))$
142	136 141	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\}])$
143		ssun2	$⊢ \{B\} \subseteq f \cup \{B\}$
144		snssg	$⊢ B \in (1 \dots B) \to (B \in (f \cup \{B\}) \leftrightarrow \{B\} \subseteq f \cup \{B\})$
145	49 144	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\})$
146	143 145	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\})$
147	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\}))$
148	51 142 146 147	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)\}$
149		vex	$⊢ f \in V$
150		snex	$⊢ \{B\} \in V$
151	149 150	unex	$⊢ f \cup \{B\} \in V$
152	8	fdmi	$⊢ dom \|.\| = V$
153	151 152	eleqtrri	$⊢ f \cup \{B\} \in dom \|.\|$
154		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)\}])$
155	10 153 154	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)\}]$
156	148 155	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)\}]$
157	156	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$
158	25	simpli	$⊢ \|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] \in Fin$
159		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$
160	29 158 159	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$
161	36 39	ltnled	$⊢ φ \to (A < B \leftrightarrow \neg B \leq A)$
162	7 161	mpbid	$⊢ φ \to \neg B \leq A$
163		elfzle2	$⊢ B \in (1 \dots A) \to B \leq A$
164	162 163	nsyl	$⊢ φ \to \neg B \in (1 \dots A)$
165	164	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)$
166	18 165	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$
167		hashunsng	$⊢ B \in (1 \dots N) \to ((f \in Fin \land \neg B \in f) \to \|f \cup \{B\}\| = \|f\| + 1)$
168	100 167	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)$
169	20 166 168	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$
170	169 156	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)\}]$
171		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)\}] ℝ <)$
172	29 157 160 170 171	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)\}] ℝ <)$
173	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)\}] ℝ <)$
174	6 173	syl	$⊢ φ \to K (B) = sup (\|.\| [\{y \in 𝒫 (1 \dots B) \| (({F ↾}_{y}) {Isom}_{<, O} (y, F [y]) \land B \in y)\}] ℝ <)$
175	174	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)\}] ℝ <)$
176	172 175	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)$
177	1 2 3 4	erdszelem6	$⊢ φ \to K : (1 \dots N) ⟶ ℕ$
178	177 6	ffvelrnd	$⊢ φ \to K (B) \in ℕ$
179	178	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 ℕ$
180	179	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}$
181		nn0ltp1le	$⊢ (\|f\| \in ℕ_{0} \land K (B) \in ℕ_{0}) \to (\|f\| < K (B) \leftrightarrow \|f\| + 1 \leq K (B))$
182	22 180 181	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))$
183	176 182	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)$
184	23 183	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)$
185	184	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))$
186		neeq1	$⊢ \|f\| = K (A) \to (\|f\| \neq K (B) \leftrightarrow K (A) \neq K (B))$
187	186	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)))$
188	185 187	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)))$
189	16 188	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)))$
190	189	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)))$
191	14 190	mpd	$⊢ φ \to (F (A) O F (B) \to K (A) \neq K (B))$
192	191	necon2bd	$⊢ φ \to (K (A) = K (B) \to \neg F (A) O F (B))$

Metamath Proof Explorer

Theorem erdszelem8

Proof