erdszelem11

	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)⟩)$
	erdszelem.r	$⊢ φ \to R \in ℕ$
	erdszelem.s	$⊢ φ \to S \in ℕ$
	erdszelem.m	$⊢ φ \to (R - 1) (S - 1) < N$
Assertion	erdszelem11	$⊢ φ \to \exists s \in 𝒫 (1 \dots N) ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])))$

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		erdszelem.r	$⊢ φ \to R \in ℕ$
7		erdszelem.s	$⊢ φ \to S \in ℕ$
8		erdszelem.m	$⊢ φ \to (R - 1) (S - 1) < N$
9	1 2 3 4 5 6 7 8	erdszelem10	$⊢ φ \to \exists m \in (1 \dots N) (\neg I (m) \in (1 \dots R - 1) \lor \neg J (m) \in (1 \dots S - 1))$
10	1	adantr	$⊢ (φ \land (m \in (1 \dots N) \land \neg I (m) \in (1 \dots R - 1))) \to N \in ℕ$
11	2	adantr	$⊢ (φ \land (m \in (1 \dots N) \land \neg I (m) \in (1 \dots R - 1))) \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
12		ltso	$⊢ < Or ℝ$
13		simprl	$⊢ (φ \land (m \in (1 \dots N) \land \neg I (m) \in (1 \dots R - 1))) \to m \in (1 \dots N)$
14	6	adantr	$⊢ (φ \land (m \in (1 \dots N) \land \neg I (m) \in (1 \dots R - 1))) \to R \in ℕ$
15		simprr	$⊢ (φ \land (m \in (1 \dots N) \land \neg I (m) \in (1 \dots R - 1))) \to \neg I (m) \in (1 \dots R - 1)$
16	10 11 3 12 13 14 15	erdszelem7	$⊢ (φ \land (m \in (1 \dots N) \land \neg I (m) \in (1 \dots R - 1))) \to \exists s \in 𝒫 (1 \dots N) (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s]))$
17	16	expr	$⊢ (φ \land m \in (1 \dots N)) \to (\neg I (m) \in (1 \dots R - 1) \to \exists s \in 𝒫 (1 \dots N) (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])))$
18	1	adantr	$⊢ (φ \land (m \in (1 \dots N) \land \neg J (m) \in (1 \dots S - 1))) \to N \in ℕ$
19	2	adantr	$⊢ (φ \land (m \in (1 \dots N) \land \neg J (m) \in (1 \dots S - 1))) \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
20		gtso	$⊢ <^{-1} Or ℝ$
21		simprl	$⊢ (φ \land (m \in (1 \dots N) \land \neg J (m) \in (1 \dots S - 1))) \to m \in (1 \dots N)$
22	7	adantr	$⊢ (φ \land (m \in (1 \dots N) \land \neg J (m) \in (1 \dots S - 1))) \to S \in ℕ$
23		simprr	$⊢ (φ \land (m \in (1 \dots N) \land \neg J (m) \in (1 \dots S - 1))) \to \neg J (m) \in (1 \dots S - 1)$
24	18 19 4 20 21 22 23	erdszelem7	$⊢ (φ \land (m \in (1 \dots N) \land \neg J (m) \in (1 \dots S - 1))) \to \exists s \in 𝒫 (1 \dots N) (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]))$
25	24	expr	$⊢ (φ \land m \in (1 \dots N)) \to (\neg J (m) \in (1 \dots S - 1) \to \exists s \in 𝒫 (1 \dots N) (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])))$
26	17 25	orim12d	$⊢ (φ \land m \in (1 \dots N)) \to ((\neg I (m) \in (1 \dots R - 1) \lor \neg J (m) \in (1 \dots S - 1)) \to (\exists s \in 𝒫 (1 \dots N) (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor \exists s \in 𝒫 (1 \dots N) (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]))))$
27	26	rexlimdva	$⊢ φ \to (\exists m \in (1 \dots N) (\neg I (m) \in (1 \dots R - 1) \lor \neg J (m) \in (1 \dots S - 1)) \to (\exists s \in 𝒫 (1 \dots N) (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor \exists s \in 𝒫 (1 \dots N) (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]))))$
28	9 27	mpd	$⊢ φ \to (\exists s \in 𝒫 (1 \dots N) (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor \exists s \in 𝒫 (1 \dots N) (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])))$
29		r19.43	$⊢ \exists s \in 𝒫 (1 \dots N) ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s]))) \leftrightarrow (\exists s \in 𝒫 (1 \dots N) (R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor \exists s \in 𝒫 (1 \dots N) (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])))$
30	28 29	sylibr	$⊢ φ \to \exists s \in 𝒫 (1 \dots N) ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])))$

Metamath Proof Explorer

Theorem erdszelem11

Proof