Metamath Proof Explorer

Theorem 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 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
Assertion dyadmax ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 ltweuz ⊢ < We ( ℤ≥ ‘ 0 )
3 2 a1i ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → < We ( ℤ≥ ‘ 0 ) )
4 nn0ex ⊢ ℕ0 ∈ V
5 4 rabex ⊢ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ∈ V
6 5 a1i ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ∈ V )
7 ssrab2 ⊢ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ⊆ ℕ0
8 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9 7 8 sseqtri ⊢ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ⊆ ( ℤ≥ ‘ 0 )
10 9 a1i ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ⊆ ( ℤ≥ ‘ 0 ) )
11 id ⊢ ( 𝐴 ≠ ∅ → 𝐴 ≠ ∅ )
12 1 dyadf ⊢ 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) )
13 ffn ⊢ ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 Fn ( ℤ × ℕ0 ) )
14 ovelrn ⊢ ( 𝐹 Fn ( ℤ × ℕ0 ) → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑛 ∈ ℕ0 𝑧 = ( 𝑎 𝐹 𝑛 ) ) )
15 12 13 14 mp2b ⊢ ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑛 ∈ ℕ0 𝑧 = ( 𝑎 𝐹 𝑛 ) )
16 rexcom ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑛 ∈ ℕ0 𝑧 = ( 𝑎 𝐹 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) )
17 15 16 sylbb ⊢ ( 𝑧 ∈ ran 𝐹 → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) )
18 17 rgen ⊢ ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 )
19 ssralv ⊢ ( 𝐴 ⊆ ran 𝐹 → ( ∀ 𝑧 ∈ ran 𝐹 ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) ) )
20 18 19 mpi ⊢ ( 𝐴 ⊆ ran 𝐹 → ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) )
21 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) ) → ∃ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) )
22 11 20 21 syl2anr ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) )
23 rexcom ⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) )
24 22 23 sylib ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) )
25 rabn0 ⊢ ( { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ≠ ∅ ↔ ∃ 𝑛 ∈ ℕ0 ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) )
26 24 25 sylibr ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ≠ ∅ )
27 wereu ⊢ ( ( < We ( ℤ≥ ‘ 0 ) ∧ ( { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ∈ V ∧ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ⊆ ( ℤ≥ ‘ 0 ) ∧ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ≠ ∅ ) ) → ∃! 𝑐 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 )
28 3 6 10 26 27 syl13anc ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ∃! 𝑐 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 )
29 reurex ⊢ ( ∃! 𝑐 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 → ∃ 𝑐 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 )
30 28 29 syl ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑐 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 )
31 oveq2 ⊢ ( 𝑛 = 𝑐 → ( 𝑎 𝐹 𝑛 ) = ( 𝑎 𝐹 𝑐 ) )
32 31 eqeq2d ⊢ ( 𝑛 = 𝑐 → ( 𝑧 = ( 𝑎 𝐹 𝑛 ) ↔ 𝑧 = ( 𝑎 𝐹 𝑐 ) ) )
33 32 2rexbidv ⊢ ( 𝑛 = 𝑐 → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑐 ) ) )
34 33 elrab ⊢ ( 𝑐 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ↔ ( 𝑐 ∈ ℕ0 ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑐 ) ) )
35 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝑎 𝐹 𝑛 ) ↔ 𝑤 = ( 𝑎 𝐹 𝑛 ) ) )
36 oveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 𝐹 𝑛 ) = ( 𝑏 𝐹 𝑛 ) )
37 36 eqeq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑤 = ( 𝑎 𝐹 𝑛 ) ↔ 𝑤 = ( 𝑏 𝐹 𝑛 ) ) )
38 35 37 cbvrex2vw ⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑛 ) )
39 oveq2 ⊢ ( 𝑛 = 𝑑 → ( 𝑏 𝐹 𝑛 ) = ( 𝑏 𝐹 𝑑 ) )
40 39 eqeq2d ⊢ ( 𝑛 = 𝑑 → ( 𝑤 = ( 𝑏 𝐹 𝑛 ) ↔ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) )
41 40 2rexbidv ⊢ ( 𝑛 = 𝑑 → ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑛 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) )
42 38 41 bitrid ⊢ ( 𝑛 = 𝑑 → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) )
43 42 ralrab ⊢ ( ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 ↔ ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) )
44 r19.23v ⊢ ( ∀ 𝑤 ∈ 𝐴 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ↔ ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) )
45 44 ralbii ⊢ ( ∀ 𝑑 ∈ ℕ0 ∀ 𝑤 ∈ 𝐴 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ↔ ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) )
46 ralcom ⊢ ( ∀ 𝑑 ∈ ℕ0 ∀ 𝑤 ∈ 𝐴 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) )
47 45 46 bitr3i ⊢ ( ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) )
48 simplll ⊢ ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) → 𝐴 ⊆ ran 𝐹 )
49 48 sselda ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ran 𝐹 )
50 ovelrn ⊢ ( 𝐹 Fn ( ℤ × ℕ0 ) → ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑏 ∈ ℤ ∃ 𝑑 ∈ ℕ0 𝑤 = ( 𝑏 𝐹 𝑑 ) ) )
51 12 13 50 mp2b ⊢ ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑏 ∈ ℤ ∃ 𝑑 ∈ ℕ0 𝑤 = ( 𝑏 𝐹 𝑑 ) )
52 49 51 sylib ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) → ∃ 𝑏 ∈ ℤ ∃ 𝑑 ∈ ℕ0 𝑤 = ( 𝑏 𝐹 𝑑 ) )
53 rexcom ⊢ ( ∃ 𝑏 ∈ ℤ ∃ 𝑑 ∈ ℕ0 𝑤 = ( 𝑏 𝐹 𝑑 ) ↔ ∃ 𝑑 ∈ ℕ0 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) )
54 r19.29 ⊢ ( ( ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ∧ ∃ 𝑑 ∈ ℕ0 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) → ∃ 𝑑 ∈ ℕ0 ( ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ∧ ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) )
55 54 expcom ⊢ ( ∃ 𝑑 ∈ ℕ0 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) → ∃ 𝑑 ∈ ℕ0 ( ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ∧ ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) ) )
56 53 55 sylbi ⊢ ( ∃ 𝑏 ∈ ℤ ∃ 𝑑 ∈ ℕ0 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) → ∃ 𝑑 ∈ ℕ0 ( ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ∧ ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) ) )
57 52 56 syl ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) → ∃ 𝑑 ∈ ℕ0 ( ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ∧ ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) ) )
58 simplrr ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) → 𝑎 ∈ ℤ )
59 58 ad2antrr ⊢ ( ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ¬ 𝑑 < 𝑐 ∧ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ) → 𝑎 ∈ ℤ )
60 simplrr ⊢ ( ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ¬ 𝑑 < 𝑐 ∧ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ) → 𝑏 ∈ ℤ )
61 simp-5r ⊢ ( ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ¬ 𝑑 < 𝑐 ∧ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ) → 𝑐 ∈ ℕ0 )
62 simplrl ⊢ ( ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ¬ 𝑑 < 𝑐 ∧ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ) → 𝑑 ∈ ℕ0 )
63 simprl ⊢ ( ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ¬ 𝑑 < 𝑐 ∧ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ) → ¬ 𝑑 < 𝑐 )
64 simprr ⊢ ( ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ¬ 𝑑 < 𝑐 ∧ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ) → ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) )
65 1 59 60 61 62 63 64 dyadmaxlem ⊢ ( ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ¬ 𝑑 < 𝑐 ∧ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ) → ( 𝑎 = 𝑏 ∧ 𝑐 = 𝑑 ) )
66 oveq12 ⊢ ( ( 𝑎 = 𝑏 ∧ 𝑐 = 𝑑 ) → ( 𝑎 𝐹 𝑐 ) = ( 𝑏 𝐹 𝑑 ) )
67 65 66 syl ⊢ ( ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ¬ 𝑑 < 𝑐 ∧ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ) → ( 𝑎 𝐹 𝑐 ) = ( 𝑏 𝐹 𝑑 ) )
68 67 exp32 ⊢ ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) → ( ¬ 𝑑 < 𝑐 → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) → ( 𝑎 𝐹 𝑐 ) = ( 𝑏 𝐹 𝑑 ) ) ) )
69 fveq2 ⊢ ( 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( [,] ‘ 𝑤 ) = ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) )
70 69 sseq2d ⊢ ( 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) )
71 eqeq2 ⊢ ( 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ( 𝑎 𝐹 𝑐 ) = 𝑤 ↔ ( 𝑎 𝐹 𝑐 ) = ( 𝑏 𝐹 𝑑 ) ) )
72 70 71 imbi12d ⊢ ( 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) → ( 𝑎 𝐹 𝑐 ) = ( 𝑏 𝐹 𝑑 ) ) ) )
73 72 imbi2d ⊢ ( 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ( ¬ 𝑑 < 𝑐 → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) ↔ ( ¬ 𝑑 < 𝑐 → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) → ( 𝑎 𝐹 𝑐 ) = ( 𝑏 𝐹 𝑑 ) ) ) ) )
74 68 73 syl5ibrcom ⊢ ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) → ( 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ¬ 𝑑 < 𝑐 → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) ) )
75 74 anassrs ⊢ ( ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑑 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) → ( 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ¬ 𝑑 < 𝑐 → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) ) )
76 75 rexlimdva ⊢ ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑑 ∈ ℕ0 ) → ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ¬ 𝑑 < 𝑐 → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) ) )
77 76 a2d ⊢ ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) → ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) ) )
78 77 impd ⊢ ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ∧ ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) )
79 78 rexlimdva ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ∃ 𝑑 ∈ ℕ0 ( ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ∧ ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) ) → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) )
80 57 79 syld ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) )
81 80 ralimdva ⊢ ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) → ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) )
82 47 81 biimtrid ⊢ ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) → ( ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) )
83 82 imp ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) ∧ ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) )
84 83 an32s ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) )
85 fveq2 ⊢ ( 𝑧 = ( 𝑎 𝐹 𝑐 ) → ( [,] ‘ 𝑧 ) = ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) )
86 85 sseq1d ⊢ ( 𝑧 = ( 𝑎 𝐹 𝑐 ) → ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) ) )
87 eqeq1 ⊢ ( 𝑧 = ( 𝑎 𝐹 𝑐 ) → ( 𝑧 = 𝑤 ↔ ( 𝑎 𝐹 𝑐 ) = 𝑤 ) )
88 86 87 imbi12d ⊢ ( 𝑧 = ( 𝑎 𝐹 𝑐 ) → ( ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) )
89 88 ralbidv ⊢ ( 𝑧 = ( 𝑎 𝐹 𝑐 ) → ( ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ 𝑤 ) → ( 𝑎 𝐹 𝑐 ) = 𝑤 ) ) )
90 84 89 syl5ibrcom ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ℤ ) ) → ( 𝑧 = ( 𝑎 𝐹 𝑐 ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
91 90 anassrs ⊢ ( ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑧 = ( 𝑎 𝐹 𝑐 ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
92 91 rexlimdva ⊢ ( ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑐 ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
93 92 reximdva ⊢ ( ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) ∧ ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) ) → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑐 ) → ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
94 93 ex ⊢ ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) → ( ∀ 𝑑 ∈ ℕ0 ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑏 ∈ ℤ 𝑤 = ( 𝑏 𝐹 𝑑 ) → ¬ 𝑑 < 𝑐 ) → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑐 ) → ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) ) )
95 43 94 biimtrid ⊢ ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) → ( ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑐 ) → ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) ) )
96 95 com23 ⊢ ( ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) ∧ 𝑐 ∈ ℕ0 ) → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑐 ) → ( ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 → ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) ) )
97 96 expimpd ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ( ( 𝑐 ∈ ℕ0 ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑐 ) ) → ( ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 → ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) ) )
98 34 97 biimtrid ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ( 𝑐 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } → ( ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 → ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) ) )
99 98 rexlimdv ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑐 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ∀ 𝑑 ∈ { 𝑛 ∈ ℕ0 ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑎 ∈ ℤ 𝑧 = ( 𝑎 𝐹 𝑛 ) } ¬ 𝑑 < 𝑐 → ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
100 30 99 mpd ⊢ ( ( 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) )