Step | Hyp | Ref
| Expression |
1 | | ineq1 4145 |
. . . . 5
⊢ (𝑢 = 𝑈 → (𝑢 ∩ 𝐴) = (𝑈 ∩ 𝐴)) |
2 | 1 | eleq1d 2825 |
. . . 4
⊢ (𝑢 = 𝑈 → ((𝑢 ∩ 𝐴) ∈ Univ ↔ (𝑈 ∩ 𝐴) ∈ Univ)) |
3 | 2 | imbi2d 341 |
. . 3
⊢ (𝑢 = 𝑈 → (((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴))) → (𝑢 ∩ 𝐴) ∈ Univ) ↔ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴))) → (𝑈 ∩ 𝐴) ∈ Univ))) |
4 | | elgrug 10549 |
. . . . . 6
⊢ (𝑢 ∈ Univ → (𝑢 ∈ Univ ↔ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢)))) |
5 | 4 | ibi 266 |
. . . . 5
⊢ (𝑢 ∈ Univ → (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))) |
6 | | trin 5206 |
. . . . . . 7
⊢ ((Tr
𝑢 ∧ Tr 𝐴) → Tr (𝑢 ∩ 𝐴)) |
7 | 6 | ex 413 |
. . . . . 6
⊢ (Tr 𝑢 → (Tr 𝐴 → Tr (𝑢 ∩ 𝐴))) |
8 | | inss1 4168 |
. . . . . . . 8
⊢ (𝑢 ∩ 𝐴) ⊆ 𝑢 |
9 | | ssralv 3992 |
. . . . . . . 8
⊢ ((𝑢 ∩ 𝐴) ⊆ 𝑢 → (∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) → ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))) |
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) → ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢)) |
11 | | inss2 4169 |
. . . . . . . 8
⊢ (𝑢 ∩ 𝐴) ⊆ 𝐴 |
12 | | ssralv 3992 |
. . . . . . . 8
⊢ ((𝑢 ∩ 𝐴) ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴)) → ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴)))) |
13 | 11, 12 | ax-mp 5 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴)) → ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴))) |
14 | | elin 3908 |
. . . . . . . . . . . . 13
⊢
(𝒫 𝑥 ∈
(𝑢 ∩ 𝐴) ↔ (𝒫 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝐴)) |
15 | 14 | simplbi2 501 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑥 ∈
𝑢 → (𝒫 𝑥 ∈ 𝐴 → 𝒫 𝑥 ∈ (𝑢 ∩ 𝐴))) |
16 | | ssralv 3992 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∩ 𝐴) ⊆ 𝑢 → (∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ 𝑢)) |
17 | 8, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝑢 {𝑥, 𝑦} ∈ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ 𝑢) |
18 | | ssralv 3992 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∩ 𝐴) ⊆ 𝐴 → (∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 → ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ 𝐴)) |
19 | 11, 18 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝐴 {𝑥, 𝑦} ∈ 𝐴 → ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ 𝐴) |
20 | | elin 3908 |
. . . . . . . . . . . . . . 15
⊢ ({𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴) ↔ ({𝑥, 𝑦} ∈ 𝑢 ∧ {𝑥, 𝑦} ∈ 𝐴)) |
21 | 20 | simplbi2 501 |
. . . . . . . . . . . . . 14
⊢ ({𝑥, 𝑦} ∈ 𝑢 → ({𝑥, 𝑦} ∈ 𝐴 → {𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴))) |
22 | 21 | ral2imi 3084 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
(𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ 𝑢 → (∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ 𝐴 → ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴))) |
23 | 17, 19, 22 | syl2im 40 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑢 {𝑥, 𝑦} ∈ 𝑢 → (∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 → ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴))) |
24 | 15, 23 | im2anan9 620 |
. . . . . . . . . . 11
⊢
((𝒫 𝑥 ∈
𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢) → ((𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴) → (𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴)))) |
25 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑢 ∈ V |
26 | | mapss 8660 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ V ∧ (𝑢 ∩ 𝐴) ⊆ 𝑢) → ((𝑢 ∩ 𝐴) ↑m 𝑥) ⊆ (𝑢 ↑m 𝑥)) |
27 | 25, 8, 26 | mp2an 689 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∩ 𝐴) ↑m 𝑥) ⊆ (𝑢 ↑m 𝑥) |
28 | | ssralv 3992 |
. . . . . . . . . . . . 13
⊢ (((𝑢 ∩ 𝐴) ↑m 𝑥) ⊆ (𝑢 ↑m 𝑥) → (∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢 → ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
(𝑢 ↑m 𝑥)∪
ran 𝑦 ∈ 𝑢 → ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) |
30 | 25 | inex1 5245 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∩ 𝐴) ∈ V |
31 | | vex 3435 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
32 | 30, 31 | elmap 8642 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥) ↔ 𝑦:𝑥⟶(𝑢 ∩ 𝐴)) |
33 | | fss 6615 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦:𝑥⟶(𝑢 ∩ 𝐴) ∧ (𝑢 ∩ 𝐴) ⊆ 𝐴) → 𝑦:𝑥⟶𝐴) |
34 | 11, 33 | mpan2 688 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦:𝑥⟶(𝑢 ∩ 𝐴) → 𝑦:𝑥⟶𝐴) |
35 | 32, 34 | sylbi 216 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥) → 𝑦:𝑥⟶𝐴) |
36 | 35 | imim1i 63 |
. . . . . . . . . . . . . 14
⊢ ((𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴) → (𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥) → ∪ ran
𝑦 ∈ 𝐴)) |
37 | 36 | alimi 1818 |
. . . . . . . . . . . . 13
⊢
(∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴) → ∀𝑦(𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥) → ∪ ran
𝑦 ∈ 𝐴)) |
38 | | df-ral 3071 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ 𝐴 ↔ ∀𝑦(𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥) → ∪ ran
𝑦 ∈ 𝐴)) |
39 | 37, 38 | sylibr 233 |
. . . . . . . . . . . 12
⊢
(∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴) → ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ 𝐴) |
40 | | elin 3908 |
. . . . . . . . . . . . . 14
⊢ (∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴) ↔ (∪ ran
𝑦 ∈ 𝑢 ∧ ∪ ran 𝑦 ∈ 𝐴)) |
41 | 40 | simplbi2 501 |
. . . . . . . . . . . . 13
⊢ (∪ ran 𝑦 ∈ 𝑢 → (∪ ran
𝑦 ∈ 𝐴 → ∪ ran
𝑦 ∈ (𝑢 ∩ 𝐴))) |
42 | 41 | ral2imi 3084 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢 → (∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ 𝐴 → ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴))) |
43 | 29, 39, 42 | syl2im 40 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
(𝑢 ↑m 𝑥)∪
ran 𝑦 ∈ 𝑢 → (∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴) → ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴))) |
44 | 24, 43 | im2anan9 620 |
. . . . . . . . . 10
⊢
(((𝒫 𝑥
∈ 𝑢 ∧
∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢) ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) → (((𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴) ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴)) → ((𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴)) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴)))) |
45 | 44 | 3impa 1109 |
. . . . . . . . 9
⊢
((𝒫 𝑥 ∈
𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) → (((𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴) ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴)) → ((𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴)) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴)))) |
46 | | df-3an 1088 |
. . . . . . . . 9
⊢
((𝒫 𝑥 ∈
𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴)) ↔ ((𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴) ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴))) |
47 | | df-3an 1088 |
. . . . . . . . 9
⊢
((𝒫 𝑥 ∈
(𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴)) ↔ ((𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴)) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴))) |
48 | 45, 46, 47 | 3imtr4g 296 |
. . . . . . . 8
⊢
((𝒫 𝑥 ∈
𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) → ((𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴)) → (𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴)))) |
49 | 48 | ral2imi 3084 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) → (∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴)) → ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴)))) |
50 | 10, 13, 49 | syl2im 40 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) → (∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴)) → ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴)))) |
51 | 7, 50 | im2anan9 620 |
. . . . 5
⊢ ((Tr
𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢)) → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴))) → (Tr (𝑢 ∩ 𝐴) ∧ ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴))))) |
52 | 5, 51 | syl 17 |
. . . 4
⊢ (𝑢 ∈ Univ → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴))) → (Tr (𝑢 ∩ 𝐴) ∧ ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴))))) |
53 | | elgrug 10549 |
. . . . 5
⊢ ((𝑢 ∩ 𝐴) ∈ V → ((𝑢 ∩ 𝐴) ∈ Univ ↔ (Tr (𝑢 ∩ 𝐴) ∧ ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴))))) |
54 | 30, 53 | ax-mp 5 |
. . . 4
⊢ ((𝑢 ∩ 𝐴) ∈ Univ ↔ (Tr (𝑢 ∩ 𝐴) ∧ ∀𝑥 ∈ (𝑢 ∩ 𝐴)(𝒫 𝑥 ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ (𝑢 ∩ 𝐴){𝑥, 𝑦} ∈ (𝑢 ∩ 𝐴) ∧ ∀𝑦 ∈ ((𝑢 ∩ 𝐴) ↑m 𝑥)∪ ran 𝑦 ∈ (𝑢 ∩ 𝐴)))) |
55 | 52, 54 | syl6ibr 251 |
. . 3
⊢ (𝑢 ∈ Univ → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴))) → (𝑢 ∩ 𝐴) ∈ Univ)) |
56 | 3, 55 | vtoclga 3512 |
. 2
⊢ (𝑈 ∈ Univ → ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴))) → (𝑈 ∩ 𝐴) ∈ Univ)) |
57 | 56 | com12 32 |
1
⊢ ((Tr
𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran
𝑦 ∈ 𝐴))) → (𝑈 ∈ Univ → (𝑈 ∩ 𝐴) ∈ Univ)) |