Step | Hyp | Ref
| Expression |
1 | | eluni2 4663 |
. . . 4
⊢ (𝑎 ∈ ∪ ([,] “ 𝐴) ↔ ∃𝑖 ∈ ([,] “ 𝐴)𝑎 ∈ 𝑖) |
2 | | iccf 12562 |
. . . . . . 7
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
3 | | ffn 6279 |
. . . . . . 7
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → [,] Fn (ℝ* ×
ℝ*)) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
⊢ [,] Fn
(ℝ* × ℝ*) |
5 | | dyadmbl.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) |
6 | | dyadmbl.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) |
7 | 6 | dyadf 23758 |
. . . . . . . . 9
⊢ 𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ ×
ℝ)) |
8 | | frn 6285 |
. . . . . . . . 9
⊢ (𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) → ran
𝐹 ⊆ ( ≤ ∩
(ℝ × ℝ))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . 8
⊢ ran 𝐹 ⊆ ( ≤ ∩ (ℝ
× ℝ)) |
10 | | inss2 4059 |
. . . . . . . . 9
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
11 | | rexpssxrxp 10402 |
. . . . . . . . 9
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
12 | 10, 11 | sstri 3837 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
13 | 9, 12 | sstri 3837 |
. . . . . . 7
⊢ ran 𝐹 ⊆ (ℝ*
× ℝ*) |
14 | 5, 13 | syl6ss 3840 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ (ℝ* ×
ℝ*)) |
15 | | eleq2 2896 |
. . . . . . 7
⊢ (𝑖 = ([,]‘𝑡) → (𝑎 ∈ 𝑖 ↔ 𝑎 ∈ ([,]‘𝑡))) |
16 | 15 | rexima 6754 |
. . . . . 6
⊢ (([,] Fn
(ℝ* × ℝ*) ∧ 𝐴 ⊆ (ℝ* ×
ℝ*)) → (∃𝑖 ∈ ([,] “ 𝐴)𝑎 ∈ 𝑖 ↔ ∃𝑡 ∈ 𝐴 𝑎 ∈ ([,]‘𝑡))) |
17 | 4, 14, 16 | sylancr 583 |
. . . . 5
⊢ (𝜑 → (∃𝑖 ∈ ([,] “ 𝐴)𝑎 ∈ 𝑖 ↔ ∃𝑡 ∈ 𝐴 𝑎 ∈ ([,]‘𝑡))) |
18 | | ssrab2 3913 |
. . . . . . . . 9
⊢ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ⊆ 𝐴 |
19 | 5 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → 𝐴 ⊆ ran 𝐹) |
20 | 18, 19 | syl5ss 3839 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ⊆ ran 𝐹) |
21 | | simprl 789 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → 𝑡 ∈ 𝐴) |
22 | | ssid 3849 |
. . . . . . . . . 10
⊢
([,]‘𝑡)
⊆ ([,]‘𝑡) |
23 | | fveq2 6434 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑡 → ([,]‘𝑎) = ([,]‘𝑡)) |
24 | 23 | sseq2d 3859 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑡 → (([,]‘𝑡) ⊆ ([,]‘𝑎) ↔ ([,]‘𝑡) ⊆ ([,]‘𝑡))) |
25 | 24 | rspcev 3527 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑡)) → ∃𝑎 ∈ 𝐴 ([,]‘𝑡) ⊆ ([,]‘𝑎)) |
26 | 21, 22, 25 | sylancl 582 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → ∃𝑎 ∈ 𝐴 ([,]‘𝑡) ⊆ ([,]‘𝑎)) |
27 | | rabn0 4188 |
. . . . . . . . 9
⊢ ({𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ≠ ∅ ↔ ∃𝑎 ∈ 𝐴 ([,]‘𝑡) ⊆ ([,]‘𝑎)) |
28 | 26, 27 | sylibr 226 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ≠ ∅) |
29 | 6 | dyadmax 23765 |
. . . . . . . 8
⊢ (({𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ⊆ ran 𝐹 ∧ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ≠ ∅) → ∃𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)}∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) |
30 | 20, 28, 29 | syl2anc 581 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → ∃𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)}∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) |
31 | | fveq2 6434 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑚 → ([,]‘𝑎) = ([,]‘𝑚)) |
32 | 31 | sseq2d 3859 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑚 → (([,]‘𝑡) ⊆ ([,]‘𝑎) ↔ ([,]‘𝑡) ⊆ ([,]‘𝑚))) |
33 | 32 | elrab 3586 |
. . . . . . . . 9
⊢ (𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ↔ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) |
34 | | simprlr 800 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → ([,]‘𝑡) ⊆ ([,]‘𝑚)) |
35 | | simplrr 798 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑎 ∈ ([,]‘𝑡)) |
36 | 34, 35 | sseldd 3829 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑎 ∈ ([,]‘𝑚)) |
37 | | simprll 799 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑚 ∈ 𝐴) |
38 | | fveq2 6434 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑤 → ([,]‘𝑎) = ([,]‘𝑤)) |
39 | 38 | sseq2d 3859 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑤 → (([,]‘𝑡) ⊆ ([,]‘𝑎) ↔ ([,]‘𝑡) ⊆ ([,]‘𝑤))) |
40 | 39 | elrab 3586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ↔ (𝑤 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑤))) |
41 | 40 | imbi1i 341 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) ↔ ((𝑤 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑤)) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
42 | | impexp 443 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑤)) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) ↔ (𝑤 ∈ 𝐴 → (([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)))) |
43 | 41, 42 | bitri 267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) ↔ (𝑤 ∈ 𝐴 → (([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)))) |
44 | | impexp 443 |
. . . . . . . . . . . . . . . . . 18
⊢
(((([,]‘𝑡)
⊆ ([,]‘𝑤) ∧
([,]‘𝑚) ⊆
([,]‘𝑤)) → 𝑚 = 𝑤) ↔ (([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
45 | | sstr2 3835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(([,]‘𝑡)
⊆ ([,]‘𝑚)
→ (([,]‘𝑚)
⊆ ([,]‘𝑤)
→ ([,]‘𝑡)
⊆ ([,]‘𝑤))) |
46 | 45 | ad2antll 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → ([,]‘𝑡) ⊆ ([,]‘𝑤))) |
47 | 46 | ancrd 549 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → (([,]‘𝑡) ⊆ ([,]‘𝑤) ∧ ([,]‘𝑚) ⊆ ([,]‘𝑤)))) |
48 | 47 | imim1d 82 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → (((([,]‘𝑡) ⊆ ([,]‘𝑤) ∧ ([,]‘𝑚) ⊆ ([,]‘𝑤)) → 𝑚 = 𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
49 | 44, 48 | syl5bir 235 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → ((([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
50 | 49 | imim2d 57 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → ((𝑤 ∈ 𝐴 → (([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → (𝑤 ∈ 𝐴 → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)))) |
51 | 43, 50 | syl5bi 234 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → ((𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) → (𝑤 ∈ 𝐴 → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)))) |
52 | 51 | ralimdv2 3171 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → (∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤) → ∀𝑤 ∈ 𝐴 (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
53 | 52 | impr 448 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → ∀𝑤 ∈ 𝐴 (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) |
54 | | fveq2 6434 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑚 → ([,]‘𝑧) = ([,]‘𝑚)) |
55 | 54 | sseq1d 3858 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑚 → (([,]‘𝑧) ⊆ ([,]‘𝑤) ↔ ([,]‘𝑚) ⊆ ([,]‘𝑤))) |
56 | | equequ1 2131 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑚 → (𝑧 = 𝑤 ↔ 𝑚 = 𝑤)) |
57 | 55, 56 | imbi12d 336 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑚 → ((([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
58 | 57 | ralbidv 3196 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑚 → (∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
59 | | dyadmbl.2 |
. . . . . . . . . . . . . 14
⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)} |
60 | 58, 59 | elrab2 3590 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ 𝐺 ↔ (𝑚 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
61 | 37, 53, 60 | sylanbrc 580 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑚 ∈ 𝐺) |
62 | | ffun 6282 |
. . . . . . . . . . . . . 14
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → Fun [,]) |
63 | 2, 62 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ Fun
[,] |
64 | | ssrab2 3913 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)} ⊆ 𝐴 |
65 | 59, 64 | eqsstri 3861 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 ⊆ 𝐴 |
66 | 65, 14 | syl5ss 3839 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ⊆ (ℝ* ×
ℝ*)) |
67 | 2 | fdmi 6289 |
. . . . . . . . . . . . . . 15
⊢ dom [,] =
(ℝ* × ℝ*) |
68 | 66, 67 | syl6sseqr 3878 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ⊆ dom [,]) |
69 | 68 | ad2antrr 719 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝐺 ⊆ dom [,]) |
70 | | funfvima2 6750 |
. . . . . . . . . . . . 13
⊢ ((Fun [,]
∧ 𝐺 ⊆ dom [,])
→ (𝑚 ∈ 𝐺 → ([,]‘𝑚) ∈ ([,] “ 𝐺))) |
71 | 63, 69, 70 | sylancr 583 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → (𝑚 ∈ 𝐺 → ([,]‘𝑚) ∈ ([,] “ 𝐺))) |
72 | 61, 71 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → ([,]‘𝑚) ∈ ([,] “ 𝐺)) |
73 | | elunii 4664 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ([,]‘𝑚) ∧ ([,]‘𝑚) ∈ ([,] “ 𝐺)) → 𝑎 ∈ ∪ ([,]
“ 𝐺)) |
74 | 36, 72, 73 | syl2anc 581 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑎 ∈ ∪ ([,]
“ 𝐺)) |
75 | 74 | exp32 413 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) → (∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤) → 𝑎 ∈ ∪ ([,]
“ 𝐺)))) |
76 | 33, 75 | syl5bi 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → (𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} → (∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤) → 𝑎 ∈ ∪ ([,]
“ 𝐺)))) |
77 | 76 | rexlimdv 3240 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → (∃𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)}∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤) → 𝑎 ∈ ∪ ([,]
“ 𝐺))) |
78 | 30, 77 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → 𝑎 ∈ ∪ ([,]
“ 𝐺)) |
79 | 78 | rexlimdvaa 3242 |
. . . . 5
⊢ (𝜑 → (∃𝑡 ∈ 𝐴 𝑎 ∈ ([,]‘𝑡) → 𝑎 ∈ ∪ ([,]
“ 𝐺))) |
80 | 17, 79 | sylbid 232 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ ([,] “ 𝐴)𝑎 ∈ 𝑖 → 𝑎 ∈ ∪ ([,]
“ 𝐺))) |
81 | 1, 80 | syl5bi 234 |
. . 3
⊢ (𝜑 → (𝑎 ∈ ∪ ([,]
“ 𝐴) → 𝑎 ∈ ∪ ([,] “ 𝐺))) |
82 | 81 | ssrdv 3834 |
. 2
⊢ (𝜑 → ∪ ([,] “ 𝐴) ⊆ ∪ ([,]
“ 𝐺)) |
83 | | imass2 5743 |
. . . 4
⊢ (𝐺 ⊆ 𝐴 → ([,] “ 𝐺) ⊆ ([,] “ 𝐴)) |
84 | 65, 83 | ax-mp 5 |
. . 3
⊢ ([,]
“ 𝐺) ⊆ ([,]
“ 𝐴) |
85 | | uniss 4682 |
. . 3
⊢ (([,]
“ 𝐺) ⊆ ([,]
“ 𝐴) → ∪ ([,] “ 𝐺) ⊆ ∪ ([,]
“ 𝐴)) |
86 | 84, 85 | mp1i 13 |
. 2
⊢ (𝜑 → ∪ ([,] “ 𝐺) ⊆ ∪ ([,]
“ 𝐴)) |
87 | 82, 86 | eqssd 3845 |
1
⊢ (𝜑 → ∪ ([,] “ 𝐴) = ∪ ([,]
“ 𝐺)) |