| Step | Hyp | Ref
| Expression |
| 1 | | eluni2 4911 |
. . . 4
⊢ (𝑎 ∈ ∪ ([,] “ 𝐴) ↔ ∃𝑖 ∈ ([,] “ 𝐴)𝑎 ∈ 𝑖) |
| 2 | | iccf 13488 |
. . . . . . 7
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
| 3 | | ffn 6736 |
. . . . . . 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 25626 |
. . . . . . . . 9
⊢ 𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ ×
ℝ)) |
| 8 | | frn 6743 |
. . . . . . . . 9
⊢ (𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) → ran
𝐹 ⊆ ( ≤ ∩
(ℝ × ℝ))) |
| 9 | 7, 8 | ax-mp 5 |
. . . . . . . 8
⊢ ran 𝐹 ⊆ ( ≤ ∩ (ℝ
× ℝ)) |
| 10 | | inss2 4238 |
. . . . . . . . 9
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 11 | | rexpssxrxp 11306 |
. . . . . . . . 9
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 12 | 10, 11 | sstri 3993 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 13 | 9, 12 | sstri 3993 |
. . . . . . 7
⊢ ran 𝐹 ⊆ (ℝ*
× ℝ*) |
| 14 | 5, 13 | sstrdi 3996 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ (ℝ* ×
ℝ*)) |
| 15 | | eleq2 2830 |
. . . . . . 7
⊢ (𝑖 = ([,]‘𝑡) → (𝑎 ∈ 𝑖 ↔ 𝑎 ∈ ([,]‘𝑡))) |
| 16 | 15 | rexima 7258 |
. . . . . 6
⊢ (([,] Fn
(ℝ* × ℝ*) ∧ 𝐴 ⊆ (ℝ* ×
ℝ*)) → (∃𝑖 ∈ ([,] “ 𝐴)𝑎 ∈ 𝑖 ↔ ∃𝑡 ∈ 𝐴 𝑎 ∈ ([,]‘𝑡))) |
| 17 | 4, 14, 16 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (∃𝑖 ∈ ([,] “ 𝐴)𝑎 ∈ 𝑖 ↔ ∃𝑡 ∈ 𝐴 𝑎 ∈ ([,]‘𝑡))) |
| 18 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ⊆ 𝐴 |
| 19 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → 𝐴 ⊆ ran 𝐹) |
| 20 | 18, 19 | sstrid 3995 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ⊆ ran 𝐹) |
| 21 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → 𝑡 ∈ 𝐴) |
| 22 | | ssid 4006 |
. . . . . . . . . 10
⊢
([,]‘𝑡)
⊆ ([,]‘𝑡) |
| 23 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑡 → ([,]‘𝑎) = ([,]‘𝑡)) |
| 24 | 23 | sseq2d 4016 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑡 → (([,]‘𝑡) ⊆ ([,]‘𝑎) ↔ ([,]‘𝑡) ⊆ ([,]‘𝑡))) |
| 25 | 24 | rspcev 3622 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑡)) → ∃𝑎 ∈ 𝐴 ([,]‘𝑡) ⊆ ([,]‘𝑎)) |
| 26 | 21, 22, 25 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → ∃𝑎 ∈ 𝐴 ([,]‘𝑡) ⊆ ([,]‘𝑎)) |
| 27 | | rabn0 4389 |
. . . . . . . . 9
⊢ ({𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ≠ ∅ ↔ ∃𝑎 ∈ 𝐴 ([,]‘𝑡) ⊆ ([,]‘𝑎)) |
| 28 | 26, 27 | sylibr 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ≠ ∅) |
| 29 | 6 | dyadmax 25633 |
. . . . . . . 8
⊢ (({𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ⊆ ran 𝐹 ∧ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ≠ ∅) → ∃𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)}∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) |
| 30 | 20, 28, 29 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → ∃𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)}∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) |
| 31 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑚 → ([,]‘𝑎) = ([,]‘𝑚)) |
| 32 | 31 | sseq2d 4016 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑚 → (([,]‘𝑡) ⊆ ([,]‘𝑎) ↔ ([,]‘𝑡) ⊆ ([,]‘𝑚))) |
| 33 | 32 | elrab 3692 |
. . . . . . . . 9
⊢ (𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ↔ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) |
| 34 | | simprlr 780 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → ([,]‘𝑡) ⊆ ([,]‘𝑚)) |
| 35 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑎 ∈ ([,]‘𝑡)) |
| 36 | 34, 35 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑎 ∈ ([,]‘𝑚)) |
| 37 | | simprll 779 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑚 ∈ 𝐴) |
| 38 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑤 → ([,]‘𝑎) = ([,]‘𝑤)) |
| 39 | 38 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑤 → (([,]‘𝑡) ⊆ ([,]‘𝑎) ↔ ([,]‘𝑡) ⊆ ([,]‘𝑤))) |
| 40 | 39 | elrab 3692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} ↔ (𝑤 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑤))) |
| 41 | 40 | imbi1i 349 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) ↔ ((𝑤 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑤)) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
| 42 | | impexp 450 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑤)) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) ↔ (𝑤 ∈ 𝐴 → (([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)))) |
| 43 | 41, 42 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) ↔ (𝑤 ∈ 𝐴 → (([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)))) |
| 44 | | impexp 450 |
. . . . . . . . . . . . . . . . . 18
⊢
(((([,]‘𝑡)
⊆ ([,]‘𝑤) ∧
([,]‘𝑚) ⊆
([,]‘𝑤)) → 𝑚 = 𝑤) ↔ (([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
| 45 | | sstr2 3990 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(([,]‘𝑡)
⊆ ([,]‘𝑚)
→ (([,]‘𝑚)
⊆ ([,]‘𝑤)
→ ([,]‘𝑡)
⊆ ([,]‘𝑤))) |
| 46 | 45 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → ([,]‘𝑡) ⊆ ([,]‘𝑤))) |
| 47 | 46 | ancrd 551 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → (([,]‘𝑡) ⊆ ([,]‘𝑤) ∧ ([,]‘𝑚) ⊆ ([,]‘𝑤)))) |
| 48 | 47 | imim1d 82 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → (((([,]‘𝑡) ⊆ ([,]‘𝑤) ∧ ([,]‘𝑚) ⊆ ([,]‘𝑤)) → 𝑚 = 𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
| 49 | 44, 48 | biimtrrid 243 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → ((([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
| 50 | 49 | imim2d 57 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → ((𝑤 ∈ 𝐴 → (([,]‘𝑡) ⊆ ([,]‘𝑤) → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → (𝑤 ∈ 𝐴 → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)))) |
| 51 | 43, 50 | biimtrid 242 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → ((𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) → (𝑤 ∈ 𝐴 → (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)))) |
| 52 | 51 | ralimdv2 3163 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ (𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚))) → (∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤) → ∀𝑤 ∈ 𝐴 (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
| 53 | 52 | impr 454 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → ∀𝑤 ∈ 𝐴 (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤)) |
| 54 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑚 → ([,]‘𝑧) = ([,]‘𝑚)) |
| 55 | 54 | sseq1d 4015 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑚 → (([,]‘𝑧) ⊆ ([,]‘𝑤) ↔ ([,]‘𝑚) ⊆ ([,]‘𝑤))) |
| 56 | | equequ1 2024 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑚 → (𝑧 = 𝑤 ↔ 𝑚 = 𝑤)) |
| 57 | 55, 56 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑚 → ((([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
| 58 | 57 | ralbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑚 → (∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
| 59 | | dyadmbl.2 |
. . . . . . . . . . . . . 14
⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)} |
| 60 | 58, 59 | elrab2 3695 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ 𝐺 ↔ (𝑚 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) |
| 61 | 37, 53, 60 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑚 ∈ 𝐺) |
| 62 | | ffun 6739 |
. . . . . . . . . . . . . 14
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → Fun [,]) |
| 63 | 2, 62 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ Fun
[,] |
| 64 | 59 | ssrab3 4082 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 ⊆ 𝐴 |
| 65 | 64, 14 | sstrid 3995 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ⊆ (ℝ* ×
ℝ*)) |
| 66 | 2 | fdmi 6747 |
. . . . . . . . . . . . . . 15
⊢ dom [,] =
(ℝ* × ℝ*) |
| 67 | 65, 66 | sseqtrrdi 4025 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ⊆ dom [,]) |
| 68 | 67 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝐺 ⊆ dom [,]) |
| 69 | | funfvima2 7251 |
. . . . . . . . . . . . 13
⊢ ((Fun [,]
∧ 𝐺 ⊆ dom [,])
→ (𝑚 ∈ 𝐺 → ([,]‘𝑚) ∈ ([,] “ 𝐺))) |
| 70 | 63, 68, 69 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → (𝑚 ∈ 𝐺 → ([,]‘𝑚) ∈ ([,] “ 𝐺))) |
| 71 | 61, 70 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → ([,]‘𝑚) ∈ ([,] “ 𝐺)) |
| 72 | | elunii 4912 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ([,]‘𝑚) ∧ ([,]‘𝑚) ∈ ([,] “ 𝐺)) → 𝑎 ∈ ∪ ([,]
“ 𝐺)) |
| 73 | 36, 71, 72 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) ∧ ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) ∧ ∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤))) → 𝑎 ∈ ∪ ([,]
“ 𝐺)) |
| 74 | 73 | exp32 420 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → ((𝑚 ∈ 𝐴 ∧ ([,]‘𝑡) ⊆ ([,]‘𝑚)) → (∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤) → 𝑎 ∈ ∪ ([,]
“ 𝐺)))) |
| 75 | 33, 74 | biimtrid 242 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → (𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} → (∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤) → 𝑎 ∈ ∪ ([,]
“ 𝐺)))) |
| 76 | 75 | rexlimdv 3153 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → (∃𝑚 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)}∀𝑤 ∈ {𝑎 ∈ 𝐴 ∣ ([,]‘𝑡) ⊆ ([,]‘𝑎)} (([,]‘𝑚) ⊆ ([,]‘𝑤) → 𝑚 = 𝑤) → 𝑎 ∈ ∪ ([,]
“ 𝐺))) |
| 77 | 30, 76 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑡 ∈ 𝐴 ∧ 𝑎 ∈ ([,]‘𝑡))) → 𝑎 ∈ ∪ ([,]
“ 𝐺)) |
| 78 | 77 | rexlimdvaa 3156 |
. . . . 5
⊢ (𝜑 → (∃𝑡 ∈ 𝐴 𝑎 ∈ ([,]‘𝑡) → 𝑎 ∈ ∪ ([,]
“ 𝐺))) |
| 79 | 17, 78 | sylbid 240 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ ([,] “ 𝐴)𝑎 ∈ 𝑖 → 𝑎 ∈ ∪ ([,]
“ 𝐺))) |
| 80 | 1, 79 | biimtrid 242 |
. . 3
⊢ (𝜑 → (𝑎 ∈ ∪ ([,]
“ 𝐴) → 𝑎 ∈ ∪ ([,] “ 𝐺))) |
| 81 | 80 | ssrdv 3989 |
. 2
⊢ (𝜑 → ∪ ([,] “ 𝐴) ⊆ ∪ ([,]
“ 𝐺)) |
| 82 | | imass2 6120 |
. . . 4
⊢ (𝐺 ⊆ 𝐴 → ([,] “ 𝐺) ⊆ ([,] “ 𝐴)) |
| 83 | 64, 82 | ax-mp 5 |
. . 3
⊢ ([,]
“ 𝐺) ⊆ ([,]
“ 𝐴) |
| 84 | | uniss 4915 |
. . 3
⊢ (([,]
“ 𝐺) ⊆ ([,]
“ 𝐴) → ∪ ([,] “ 𝐺) ⊆ ∪ ([,]
“ 𝐴)) |
| 85 | 83, 84 | mp1i 13 |
. 2
⊢ (𝜑 → ∪ ([,] “ 𝐺) ⊆ ∪ ([,]
“ 𝐴)) |
| 86 | 81, 85 | eqssd 4001 |
1
⊢ (𝜑 → ∪ ([,] “ 𝐴) = ∪ ([,]
“ 𝐺)) |