Step | Hyp | Ref
| Expression |
1 | | ustex2sym 22968 |
. . . 4
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑣 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) |
2 | 1 | ad4ant13 751 |
. . 3
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) |
3 | | simprl 771 |
. . . . . 6
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) ∧ (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) → ◡𝑤 = 𝑤) |
4 | | simp-5l 785 |
. . . . . . . . 9
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) ∧ (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) → 𝑈 ∈ (UnifOn‘𝑋)) |
5 | | simplr 769 |
. . . . . . . . 9
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) ∧ (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) → 𝑤 ∈ 𝑈) |
6 | | ustssco 22966 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → 𝑤 ⊆ (𝑤 ∘ 𝑤)) |
7 | 4, 5, 6 | syl2anc 587 |
. . . . . . . 8
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) ∧ (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) → 𝑤 ⊆ (𝑤 ∘ 𝑤)) |
8 | | simprr 773 |
. . . . . . . 8
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) ∧ (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) → (𝑤 ∘ 𝑤) ⊆ 𝑣) |
9 | | coss2 5699 |
. . . . . . . . . 10
⊢ ((𝑤 ∘ 𝑤) ⊆ 𝑣 → (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ (𝑤 ∘ 𝑣)) |
10 | 9 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑤 ⊆ (𝑤 ∘ 𝑤) ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣) → (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ (𝑤 ∘ 𝑣)) |
11 | | sstr 3885 |
. . . . . . . . . 10
⊢ ((𝑤 ⊆ (𝑤 ∘ 𝑤) ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣) → 𝑤 ⊆ 𝑣) |
12 | | coss1 5698 |
. . . . . . . . . 10
⊢ (𝑤 ⊆ 𝑣 → (𝑤 ∘ 𝑣) ⊆ (𝑣 ∘ 𝑣)) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ ((𝑤 ⊆ (𝑤 ∘ 𝑤) ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣) → (𝑤 ∘ 𝑣) ⊆ (𝑣 ∘ 𝑣)) |
14 | 10, 13 | sstrd 3887 |
. . . . . . . 8
⊢ ((𝑤 ⊆ (𝑤 ∘ 𝑤) ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣) → (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ (𝑣 ∘ 𝑣)) |
15 | 7, 8, 14 | syl2anc 587 |
. . . . . . 7
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) ∧ (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) → (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ (𝑣 ∘ 𝑣)) |
16 | | simpllr 776 |
. . . . . . 7
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) ∧ (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) → (𝑣 ∘ 𝑣) ⊆ 𝑉) |
17 | 15, 16 | sstrd 3887 |
. . . . . 6
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) ∧ (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) → (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ 𝑉) |
18 | 3, 17 | jca 515 |
. . . . 5
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) ∧ (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣)) → (◡𝑤 = 𝑤 ∧ (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ 𝑉)) |
19 | 18 | ex 416 |
. . . 4
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) ∧ 𝑤 ∈ 𝑈) → ((◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣) → (◡𝑤 = 𝑤 ∧ (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ 𝑉))) |
20 | 19 | reximdva 3184 |
. . 3
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) → (∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑣) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ 𝑉))) |
21 | 2, 20 | mpd 15 |
. 2
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ (𝑣 ∘ 𝑣) ⊆ 𝑉) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ 𝑉)) |
22 | | ustexhalf 22962 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑣 ∈ 𝑈 (𝑣 ∘ 𝑣) ⊆ 𝑉) |
23 | 21, 22 | r19.29a 3199 |
1
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ 𝑉)) |