Metamath Proof Explorer

Theorem dyadmbllem

Description: Lemma for dyadmbl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
dyadmbl.2 ⊢ 𝐺 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) }
dyadmbl.3 ⊢ ( 𝜑 → 𝐴 ⊆ ran 𝐹 )
Assertion dyadmbllem ( 𝜑 → ∪ ( [,] “ 𝐴 ) = ∪ ( [,] “ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 dyadmbl.2 ⊢ 𝐺 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) }
3 dyadmbl.3 ⊢ ( 𝜑 → 𝐴 ⊆ ran 𝐹 )
4 eluni2 ⊢ ( 𝑎 ∈ ∪ ( [,] “ 𝐴 ) ↔ ∃ 𝑖 ∈ ( [,] “ 𝐴 ) 𝑎 ∈ 𝑖 )
5 iccf ⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
6 ffn ⊢ ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → [,] Fn ( ℝ* × ℝ* ) )
7 5 6 ax-mp ⊢ [,] Fn ( ℝ* × ℝ* )
8 1 dyadf ⊢ 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) )
9 frn ⊢ ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) )
10 8 9 ax-mp ⊢ ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) )
11 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
12 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
13 11 12 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
14 10 13 sstri ⊢ ran 𝐹 ⊆ ( ℝ* × ℝ* )
15 3 14 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ* × ℝ* ) )
16 eleq2 ⊢ ( 𝑖 = ( [,] ‘ 𝑡 ) → ( 𝑎 ∈ 𝑖 ↔ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) )
17 16 rexima ⊢ ( ( [,] Fn ( ℝ* × ℝ* ) ∧ 𝐴 ⊆ ( ℝ* × ℝ* ) ) → ( ∃ 𝑖 ∈ ( [,] “ 𝐴 ) 𝑎 ∈ 𝑖 ↔ ∃ 𝑡 ∈ 𝐴 𝑎 ∈ ( [,] ‘ 𝑡 ) ) )
18 7 15 17 sylancr ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( [,] “ 𝐴 ) 𝑎 ∈ 𝑖 ↔ ∃ 𝑡 ∈ 𝐴 𝑎 ∈ ( [,] ‘ 𝑡 ) ) )
19 ssrab2 ⊢ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ⊆ 𝐴
20 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → 𝐴 ⊆ ran 𝐹 )
21 19 20 sstrid ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ⊆ ran 𝐹 )
22 simprl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → 𝑡 ∈ 𝐴 )
23 ssid ⊢ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑡 )
24 fveq2 ⊢ ( 𝑎 = 𝑡 → ( [,] ‘ 𝑎 ) = ( [,] ‘ 𝑡 ) )
25 24 sseq2d ⊢ ( 𝑎 = 𝑡 → ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) ↔ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑡 ) ) )
26 25 rspcev ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑡 ) ) → ∃ 𝑎 ∈ 𝐴 ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) )
27 22 23 26 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → ∃ 𝑎 ∈ 𝐴 ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) )
28 rabn0 ⊢ ( { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ≠ ∅ ↔ ∃ 𝑎 ∈ 𝐴 ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) )
29 27 28 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ≠ ∅ )
30 1 dyadmax ⊢ ( ( { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ⊆ ran 𝐹 ∧ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ≠ ∅ ) → ∃ 𝑚 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) )
31 21 29 30 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → ∃ 𝑚 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) )
32 fveq2 ⊢ ( 𝑎 = 𝑚 → ( [,] ‘ 𝑎 ) = ( [,] ‘ 𝑚 ) )
33 32 sseq2d ⊢ ( 𝑎 = 𝑚 → ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) ↔ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) )
34 33 elrab ⊢ ( 𝑚 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ↔ ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) )
35 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) )
36 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → 𝑎 ∈ ( [,] ‘ 𝑡 ) )
37 35 36 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → 𝑎 ∈ ( [,] ‘ 𝑚 ) )
38 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → 𝑚 ∈ 𝐴 )
39 fveq2 ⊢ ( 𝑎 = 𝑤 → ( [,] ‘ 𝑎 ) = ( [,] ‘ 𝑤 ) )
40 39 sseq2d ⊢ ( 𝑎 = 𝑤 → ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) ↔ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) ) )
41 40 elrab ⊢ ( 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ↔ ( 𝑤 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) ) )
42 41 imbi1i ⊢ ( ( 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ↔ ( ( 𝑤 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) )
43 impexp ⊢ ( ( ( 𝑤 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ↔ ( 𝑤 ∈ 𝐴 → ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) )
44 42 43 bitri ⊢ ( ( 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ↔ ( 𝑤 ∈ 𝐴 → ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) )
45 impexp ⊢ ( ( ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) ∧ ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) ) → 𝑚 = 𝑤 ) ↔ ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) )
46 sstr2 ⊢ ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) ) )
47 46 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) ) )
48 47 ancrd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) ∧ ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) ) ) )
49 48 imim1d ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ) → ( ( ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) ∧ ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) ) → 𝑚 = 𝑤 ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) )
50 45 49 biimtrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ) → ( ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) )
51 50 imim2d ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ) → ( ( 𝑤 ∈ 𝐴 → ( ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑤 ) → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → ( 𝑤 ∈ 𝐴 → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) )
52 44 51 biimtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ) → ( ( 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) → ( 𝑤 ∈ 𝐴 → ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) )
53 52 ralimdv2 ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ) → ( ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) )
54 53 impr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) )
55 fveq2 ⊢ ( 𝑧 = 𝑚 → ( [,] ‘ 𝑧 ) = ( [,] ‘ 𝑚 ) )
56 55 sseq1d ⊢ ( 𝑧 = 𝑚 → ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) ↔ ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) ) )
57 equequ1 ⊢ ( 𝑧 = 𝑚 → ( 𝑧 = 𝑤 ↔ 𝑚 = 𝑤 ) )
58 56 57 imbi12d ⊢ ( 𝑧 = 𝑚 → ( ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) )
59 58 ralbidv ⊢ ( 𝑧 = 𝑚 → ( ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑧 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) )
60 59 2 elrab2 ⊢ ( 𝑚 ∈ 𝐺 ↔ ( 𝑚 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) )
61 38 54 60 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → 𝑚 ∈ 𝐺 )
62 ffun ⊢ ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → Fun [,] )
63 5 62 ax-mp ⊢ Fun [,]
64 2 ssrab3 ⊢ 𝐺 ⊆ 𝐴
65 64 15 sstrid ⊢ ( 𝜑 → 𝐺 ⊆ ( ℝ* × ℝ* ) )
66 5 fdmi ⊢ dom [,] = ( ℝ* × ℝ* )
67 65 66 sseqtrrdi ⊢ ( 𝜑 → 𝐺 ⊆ dom [,] )
68 67 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → 𝐺 ⊆ dom [,] )
69 funfvima2 ⊢ ( ( Fun [,] ∧ 𝐺 ⊆ dom [,] ) → ( 𝑚 ∈ 𝐺 → ( [,] ‘ 𝑚 ) ∈ ( [,] “ 𝐺 ) ) )
70 63 68 69 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → ( 𝑚 ∈ 𝐺 → ( [,] ‘ 𝑚 ) ∈ ( [,] “ 𝐺 ) ) )
71 61 70 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → ( [,] ‘ 𝑚 ) ∈ ( [,] “ 𝐺 ) )
72 elunii ⊢ ( ( 𝑎 ∈ ( [,] ‘ 𝑚 ) ∧ ( [,] ‘ 𝑚 ) ∈ ( [,] “ 𝐺 ) ) → 𝑎 ∈ ∪ ( [,] “ 𝐺 ) )
73 37 71 72 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) ∧ ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) ∧ ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) ) ) → 𝑎 ∈ ∪ ( [,] “ 𝐺 ) )
74 73 exp32 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → ( ( 𝑚 ∈ 𝐴 ∧ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑚 ) ) → ( ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) → 𝑎 ∈ ∪ ( [,] “ 𝐺 ) ) ) )
75 34 74 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → ( 𝑚 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } → ( ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) → 𝑎 ∈ ∪ ( [,] “ 𝐺 ) ) ) )
76 75 rexlimdv ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → ( ∃ 𝑚 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ∀ 𝑤 ∈ { 𝑎 ∈ 𝐴 ∣ ( [,] ‘ 𝑡 ) ⊆ ( [,] ‘ 𝑎 ) } ( ( [,] ‘ 𝑚 ) ⊆ ( [,] ‘ 𝑤 ) → 𝑚 = 𝑤 ) → 𝑎 ∈ ∪ ( [,] “ 𝐺 ) ) )
77 31 76 mpd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ( [,] ‘ 𝑡 ) ) ) → 𝑎 ∈ ∪ ( [,] “ 𝐺 ) )
78 77 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐴 𝑎 ∈ ( [,] ‘ 𝑡 ) → 𝑎 ∈ ∪ ( [,] “ 𝐺 ) ) )
79 18 78 sylbid ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( [,] “ 𝐴 ) 𝑎 ∈ 𝑖 → 𝑎 ∈ ∪ ( [,] “ 𝐺 ) ) )
80 4 79 biimtrid ⊢ ( 𝜑 → ( 𝑎 ∈ ∪ ( [,] “ 𝐴 ) → 𝑎 ∈ ∪ ( [,] “ 𝐺 ) ) )
81 80 ssrdv ⊢ ( 𝜑 → ∪ ( [,] “ 𝐴 ) ⊆ ∪ ( [,] “ 𝐺 ) )
82 imass2 ⊢ ( 𝐺 ⊆ 𝐴 → ( [,] “ 𝐺 ) ⊆ ( [,] “ 𝐴 ) )
83 64 82 ax-mp ⊢ ( [,] “ 𝐺 ) ⊆ ( [,] “ 𝐴 )
84 uniss ⊢ ( ( [,] “ 𝐺 ) ⊆ ( [,] “ 𝐴 ) → ∪ ( [,] “ 𝐺 ) ⊆ ∪ ( [,] “ 𝐴 ) )
85 83 84 mp1i ⊢ ( 𝜑 → ∪ ( [,] “ 𝐺 ) ⊆ ∪ ( [,] “ 𝐴 ) )
86 81 85 eqssd ⊢ ( 𝜑 → ∪ ( [,] “ 𝐴 ) = ∪ ( [,] “ 𝐺 ) )