dyadmax

Description: Any nonempty set of dyadic rational intervals has a maximal element. (Contributed by Mario Carneiro, 26-Mar-2015)

		Ref	Expression
	Hypothesis	dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
	Assertion	dyadmax	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to \exists z \in A \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)$

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
2		ltweuz	$⊢ < We ℤ_{\geq 0}$
3	2	a1i	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to < We ℤ_{\geq 0}$
4		nn0ex	$⊢ ℕ_{0} \in V$
5	4	rabex	$⊢ \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \in V$
6	5	a1i	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \in V$
7		ssrab2	$⊢ \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \subseteq ℕ_{0}$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9	7 8	sseqtri	$⊢ \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \subseteq ℤ_{\geq 0}$
10	9	a1i	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \subseteq ℤ_{\geq 0}$
11		id	$⊢ A \neq \emptyset \to A \neq \emptyset$
12	1	dyadf	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$
13		ffn	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to F Fn (ℤ \times ℕ_{0})$
14		ovelrn	$⊢ F Fn (ℤ \times ℕ_{0}) \to (z \in ran F \leftrightarrow \exists a \in ℤ \exists n \in ℕ_{0} z = a F n)$
15	12 13 14	mp2b	$⊢ z \in ran F \leftrightarrow \exists a \in ℤ \exists n \in ℕ_{0} z = a F n$
16		rexcom	$⊢ \exists a \in ℤ \exists n \in ℕ_{0} z = a F n \leftrightarrow \exists n \in ℕ_{0} \exists a \in ℤ z = a F n$
17	15 16	sylbb	$⊢ z \in ran F \to \exists n \in ℕ_{0} \exists a \in ℤ z = a F n$
18	17	rgen	$⊢ \forall z \in ran F \exists n \in ℕ_{0} \exists a \in ℤ z = a F n$
19		ssralv	$⊢ A \subseteq ran F \to (\forall z \in ran F \exists n \in ℕ_{0} \exists a \in ℤ z = a F n \to \forall z \in A \exists n \in ℕ_{0} \exists a \in ℤ z = a F n)$
20	18 19	mpi	$⊢ A \subseteq ran F \to \forall z \in A \exists n \in ℕ_{0} \exists a \in ℤ z = a F n$
21		r19.2z	$⊢ (A \neq \emptyset \land \forall z \in A \exists n \in ℕ_{0} \exists a \in ℤ z = a F n) \to \exists z \in A \exists n \in ℕ_{0} \exists a \in ℤ z = a F n$
22	11 20 21	syl2anr	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to \exists z \in A \exists n \in ℕ_{0} \exists a \in ℤ z = a F n$
23		rexcom	$⊢ \exists z \in A \exists n \in ℕ_{0} \exists a \in ℤ z = a F n \leftrightarrow \exists n \in ℕ_{0} \exists z \in A \exists a \in ℤ z = a F n$
24	22 23	sylib	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to \exists n \in ℕ_{0} \exists z \in A \exists a \in ℤ z = a F n$
25		rabn0	$⊢ \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neq \emptyset \leftrightarrow \exists n \in ℕ_{0} \exists z \in A \exists a \in ℤ z = a F n$
26	24 25	sylibr	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neq \emptyset$
27		wereu	$⊢ (< We ℤ_{\geq 0} \land (\{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \in V \land \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \subseteq ℤ_{\geq 0} \land \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neq \emptyset)) \to \exists! c \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c$
28	3 6 10 26 27	syl13anc	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to \exists! c \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c$
29		reurex	$⊢ \exists! c \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c \to \exists c \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c$
30	28 29	syl	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to \exists c \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c$
31		oveq2	$⊢ n = c \to a F n = a F c$
32	31	eqeq2d	$⊢ n = c \to (z = a F n \leftrightarrow z = a F c)$
33	32	2rexbidv	$⊢ n = c \to (\exists z \in A \exists a \in ℤ z = a F n \leftrightarrow \exists z \in A \exists a \in ℤ z = a F c)$
34	33	elrab	$⊢ c \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \leftrightarrow (c \in ℕ_{0} \land \exists z \in A \exists a \in ℤ z = a F c)$
35		eqeq1	$⊢ z = w \to (z = a F n \leftrightarrow w = a F n)$
36		oveq1	$⊢ a = b \to a F n = b F n$
37	36	eqeq2d	$⊢ a = b \to (w = a F n \leftrightarrow w = b F n)$
38	35 37	cbvrex2vw	$⊢ \exists z \in A \exists a \in ℤ z = a F n \leftrightarrow \exists w \in A \exists b \in ℤ w = b F n$
39		oveq2	$⊢ n = d \to b F n = b F d$
40	39	eqeq2d	$⊢ n = d \to (w = b F n \leftrightarrow w = b F d)$
41	40	2rexbidv	$⊢ n = d \to (\exists w \in A \exists b \in ℤ w = b F n \leftrightarrow \exists w \in A \exists b \in ℤ w = b F d)$
42	38 41	bitrid	$⊢ n = d \to (\exists z \in A \exists a \in ℤ z = a F n \leftrightarrow \exists w \in A \exists b \in ℤ w = b F d)$
43	42	ralrab	$⊢ \forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c \leftrightarrow \forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c)$
44		r19.23v	$⊢ \forall w \in A (\exists b \in ℤ w = b F d \to \neg d < c) \leftrightarrow (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c)$
45	44	ralbii	$⊢ \forall d \in ℕ_{0} \forall w \in A (\exists b \in ℤ w = b F d \to \neg d < c) \leftrightarrow \forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c)$
46		ralcom	$⊢ \forall d \in ℕ_{0} \forall w \in A (\exists b \in ℤ w = b F d \to \neg d < c) \leftrightarrow \forall w \in A \forall d \in ℕ_{0} (\exists b \in ℤ w = b F d \to \neg d < c)$
47	45 46	bitr3i	$⊢ \forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c) \leftrightarrow \forall w \in A \forall d \in ℕ_{0} (\exists b \in ℤ w = b F d \to \neg d < c)$
48		simplll	$⊢ (((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \to A \subseteq ran F$
49	48	sselda	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \to w \in ran F$
50		ovelrn	$⊢ F Fn (ℤ \times ℕ_{0}) \to (w \in ran F \leftrightarrow \exists b \in ℤ \exists d \in ℕ_{0} w = b F d)$
51	12 13 50	mp2b	$⊢ w \in ran F \leftrightarrow \exists b \in ℤ \exists d \in ℕ_{0} w = b F d$
52	49 51	sylib	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \to \exists b \in ℤ \exists d \in ℕ_{0} w = b F d$
53		rexcom	$⊢ \exists b \in ℤ \exists d \in ℕ_{0} w = b F d \leftrightarrow \exists d \in ℕ_{0} \exists b \in ℤ w = b F d$
54		r19.29	$⊢ (\forall d \in ℕ_{0} (\exists b \in ℤ w = b F d \to \neg d < c) \land \exists d \in ℕ_{0} \exists b \in ℤ w = b F d) \to \exists d \in ℕ_{0} ((\exists b \in ℤ w = b F d \to \neg d < c) \land \exists b \in ℤ w = b F d)$
55	54	expcom	$⊢ \exists d \in ℕ_{0} \exists b \in ℤ w = b F d \to (\forall d \in ℕ_{0} (\exists b \in ℤ w = b F d \to \neg d < c) \to \exists d \in ℕ_{0} ((\exists b \in ℤ w = b F d \to \neg d < c) \land \exists b \in ℤ w = b F d))$
56	53 55	sylbi	$⊢ \exists b \in ℤ \exists d \in ℕ_{0} w = b F d \to (\forall d \in ℕ_{0} (\exists b \in ℤ w = b F d \to \neg d < c) \to \exists d \in ℕ_{0} ((\exists b \in ℤ w = b F d \to \neg d < c) \land \exists b \in ℤ w = b F d))$
57	52 56	syl	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \to (\forall d \in ℕ_{0} (\exists b \in ℤ w = b F d \to \neg d < c) \to \exists d \in ℕ_{0} ((\exists b \in ℤ w = b F d \to \neg d < c) \land \exists b \in ℤ w = b F d))$
58		simplrr	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \to a \in ℤ$
59	58	ad2antrr	$⊢ ((((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \land (\neg d < c \land [.] (a F c) \subseteq [.] (b F d))) \to a \in ℤ$
60		simplrr	$⊢ ((((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \land (\neg d < c \land [.] (a F c) \subseteq [.] (b F d))) \to b \in ℤ$
61		simp-5r	$⊢ ((((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \land (\neg d < c \land [.] (a F c) \subseteq [.] (b F d))) \to c \in ℕ_{0}$
62		simplrl	$⊢ ((((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \land (\neg d < c \land [.] (a F c) \subseteq [.] (b F d))) \to d \in ℕ_{0}$
63		simprl	$⊢ ((((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \land (\neg d < c \land [.] (a F c) \subseteq [.] (b F d))) \to \neg d < c$
64		simprr	$⊢ ((((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \land (\neg d < c \land [.] (a F c) \subseteq [.] (b F d))) \to [.] (a F c) \subseteq [.] (b F d)$
65	1 59 60 61 62 63 64	dyadmaxlem	$⊢ ((((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \land (\neg d < c \land [.] (a F c) \subseteq [.] (b F d))) \to (a = b \land c = d)$
66		oveq12	$⊢ (a = b \land c = d) \to a F c = b F d$
67	65 66	syl	$⊢ ((((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \land (\neg d < c \land [.] (a F c) \subseteq [.] (b F d))) \to a F c = b F d$
68	67	exp32	$⊢ (((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \to (\neg d < c \to ([.] (a F c) \subseteq [.] (b F d) \to a F c = b F d))$
69		fveq2	$⊢ w = b F d \to [.] (w) = [.] (b F d)$
70	69	sseq2d	$⊢ w = b F d \to ([.] (a F c) \subseteq [.] (w) \leftrightarrow [.] (a F c) \subseteq [.] (b F d))$
71		eqeq2	$⊢ w = b F d \to (a F c = w \leftrightarrow a F c = b F d)$
72	70 71	imbi12d	$⊢ w = b F d \to (([.] (a F c) \subseteq [.] (w) \to a F c = w) \leftrightarrow ([.] (a F c) \subseteq [.] (b F d) \to a F c = b F d))$
73	72	imbi2d	$⊢ w = b F d \to ((\neg d < c \to ([.] (a F c) \subseteq [.] (w) \to a F c = w)) \leftrightarrow (\neg d < c \to ([.] (a F c) \subseteq [.] (b F d) \to a F c = b F d)))$
74	68 73	syl5ibrcom	$⊢ (((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land (d \in ℕ_{0} \land b \in ℤ)) \to (w = b F d \to (\neg d < c \to ([.] (a F c) \subseteq [.] (w) \to a F c = w)))$
75	74	anassrs	$⊢ ((((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land d \in ℕ_{0}) \land b \in ℤ) \to (w = b F d \to (\neg d < c \to ([.] (a F c) \subseteq [.] (w) \to a F c = w)))$
76	75	rexlimdva	$⊢ (((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land d \in ℕ_{0}) \to (\exists b \in ℤ w = b F d \to (\neg d < c \to ([.] (a F c) \subseteq [.] (w) \to a F c = w)))$
77	76	a2d	$⊢ (((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land d \in ℕ_{0}) \to ((\exists b \in ℤ w = b F d \to \neg d < c) \to (\exists b \in ℤ w = b F d \to ([.] (a F c) \subseteq [.] (w) \to a F c = w)))$
78	77	impd	$⊢ (((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \land d \in ℕ_{0}) \to (((\exists b \in ℤ w = b F d \to \neg d < c) \land \exists b \in ℤ w = b F d) \to ([.] (a F c) \subseteq [.] (w) \to a F c = w))$
79	78	rexlimdva	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \to (\exists d \in ℕ_{0} ((\exists b \in ℤ w = b F d \to \neg d < c) \land \exists b \in ℤ w = b F d) \to ([.] (a F c) \subseteq [.] (w) \to a F c = w))$
80	57 79	syld	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land w \in A) \to (\forall d \in ℕ_{0} (\exists b \in ℤ w = b F d \to \neg d < c) \to ([.] (a F c) \subseteq [.] (w) \to a F c = w))$
81	80	ralimdva	$⊢ (((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \to (\forall w \in A \forall d \in ℕ_{0} (\exists b \in ℤ w = b F d \to \neg d < c) \to \forall w \in A ([.] (a F c) \subseteq [.] (w) \to a F c = w))$
82	47 81	biimtrid	$⊢ (((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \to (\forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c) \to \forall w \in A ([.] (a F c) \subseteq [.] (w) \to a F c = w))$
83	82	imp	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land (z \in A \land a \in ℤ)) \land \forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c)) \to \forall w \in A ([.] (a F c) \subseteq [.] (w) \to a F c = w)$
84	83	an32s	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land \forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c)) \land (z \in A \land a \in ℤ)) \to \forall w \in A ([.] (a F c) \subseteq [.] (w) \to a F c = w)$
85		fveq2	$⊢ z = a F c \to [.] (z) = [.] (a F c)$
86	85	sseq1d	$⊢ z = a F c \to ([.] (z) \subseteq [.] (w) \leftrightarrow [.] (a F c) \subseteq [.] (w))$
87		eqeq1	$⊢ z = a F c \to (z = w \leftrightarrow a F c = w)$
88	86 87	imbi12d	$⊢ z = a F c \to (([.] (z) \subseteq [.] (w) \to z = w) \leftrightarrow ([.] (a F c) \subseteq [.] (w) \to a F c = w))$
89	88	ralbidv	$⊢ z = a F c \to (\forall w \in A ([.] (z) \subseteq [.] (w) \to z = w) \leftrightarrow \forall w \in A ([.] (a F c) \subseteq [.] (w) \to a F c = w))$
90	84 89	syl5ibrcom	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land \forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c)) \land (z \in A \land a \in ℤ)) \to (z = a F c \to \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w))$
91	90	anassrs	$⊢ (((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land \forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c)) \land z \in A) \land a \in ℤ) \to (z = a F c \to \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w))$
92	91	rexlimdva	$⊢ ((((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land \forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c)) \land z \in A) \to (\exists a \in ℤ z = a F c \to \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w))$
93	92	reximdva	$⊢ (((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \land \forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c)) \to (\exists z \in A \exists a \in ℤ z = a F c \to \exists z \in A \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w))$
94	93	ex	$⊢ ((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \to (\forall d \in ℕ_{0} (\exists w \in A \exists b \in ℤ w = b F d \to \neg d < c) \to (\exists z \in A \exists a \in ℤ z = a F c \to \exists z \in A \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)))$
95	43 94	biimtrid	$⊢ ((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \to (\forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c \to (\exists z \in A \exists a \in ℤ z = a F c \to \exists z \in A \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)))$
96	95	com23	$⊢ ((A \subseteq ran F \land A \neq \emptyset) \land c \in ℕ_{0}) \to (\exists z \in A \exists a \in ℤ z = a F c \to (\forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c \to \exists z \in A \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)))$
97	96	expimpd	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to ((c \in ℕ_{0} \land \exists z \in A \exists a \in ℤ z = a F c) \to (\forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c \to \exists z \in A \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)))$
98	34 97	biimtrid	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to (c \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \to (\forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c \to \exists z \in A \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)))$
99	98	rexlimdv	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to (\exists c \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \forall d \in \{n \in ℕ_{0} \| \exists z \in A \exists a \in ℤ z = a F n\} \neg d < c \to \exists z \in A \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w))$
100	30 99	mpd	$⊢ (A \subseteq ran F \land A \neq \emptyset) \to \exists z \in A \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)$

Metamath Proof Explorer

Theorem dyadmax

Proof