Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . 3
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) |
2 | | intex 5206 |
. . 3
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴
∈ V) |
3 | 1, 2 | sylib 221 |
. 2
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ V) |
4 | | dfss3 3866 |
. . . . 5
⊢ (𝐴 ⊆ Univ ↔
∀𝑢 ∈ 𝐴 𝑢 ∈ Univ) |
5 | | grutr 10296 |
. . . . . 6
⊢ (𝑢 ∈ Univ → Tr 𝑢) |
6 | 5 | ralimi 3076 |
. . . . 5
⊢
(∀𝑢 ∈
𝐴 𝑢 ∈ Univ → ∀𝑢 ∈ 𝐴 Tr 𝑢) |
7 | 4, 6 | sylbi 220 |
. . . 4
⊢ (𝐴 ⊆ Univ →
∀𝑢 ∈ 𝐴 Tr 𝑢) |
8 | | trint 5153 |
. . . 4
⊢
(∀𝑢 ∈
𝐴 Tr 𝑢 → Tr ∩ 𝐴) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝐴 ⊆ Univ → Tr ∩ 𝐴) |
10 | 9 | adantr 484 |
. 2
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → Tr ∩ 𝐴) |
11 | | grupw 10298 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ Univ ∧ 𝑥 ∈ 𝑢) → 𝒫 𝑥 ∈ 𝑢) |
12 | 11 | ex 416 |
. . . . . . . . 9
⊢ (𝑢 ∈ Univ → (𝑥 ∈ 𝑢 → 𝒫 𝑥 ∈ 𝑢)) |
13 | 12 | ral2imi 3072 |
. . . . . . . 8
⊢
(∀𝑢 ∈
𝐴 𝑢 ∈ Univ → (∀𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 → ∀𝑢 ∈ 𝐴 𝒫 𝑥 ∈ 𝑢)) |
14 | | vex 3403 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
15 | 14 | elint2 4844 |
. . . . . . . 8
⊢ (𝑥 ∈ ∩ 𝐴
↔ ∀𝑢 ∈
𝐴 𝑥 ∈ 𝑢) |
16 | | vpwex 5245 |
. . . . . . . . 9
⊢ 𝒫
𝑥 ∈ V |
17 | 16 | elint2 4844 |
. . . . . . . 8
⊢
(𝒫 𝑥 ∈
∩ 𝐴 ↔ ∀𝑢 ∈ 𝐴 𝒫 𝑥 ∈ 𝑢) |
18 | 13, 15, 17 | 3imtr4g 299 |
. . . . . . 7
⊢
(∀𝑢 ∈
𝐴 𝑢 ∈ Univ → (𝑥 ∈ ∩ 𝐴 → 𝒫 𝑥 ∈ ∩ 𝐴)) |
19 | 18 | imp 410 |
. . . . . 6
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝑥 ∈ ∩ 𝐴) → 𝒫 𝑥 ∈ ∩ 𝐴) |
20 | 19 | adantlr 715 |
. . . . 5
⊢
(((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴) → 𝒫 𝑥 ∈ ∩ 𝐴) |
21 | | r19.26 3085 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
𝐴 (𝑢 ∈ Univ ∧ 𝑥 ∈ 𝑢) ↔ (∀𝑢 ∈ 𝐴 𝑢 ∈ Univ ∧ ∀𝑢 ∈ 𝐴 𝑥 ∈ 𝑢)) |
22 | | grupr 10300 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ Univ ∧ 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢) → {𝑥, 𝑦} ∈ 𝑢) |
23 | 22 | 3expia 1122 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ Univ ∧ 𝑥 ∈ 𝑢) → (𝑦 ∈ 𝑢 → {𝑥, 𝑦} ∈ 𝑢)) |
24 | 23 | ral2imi 3072 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
𝐴 (𝑢 ∈ Univ ∧ 𝑥 ∈ 𝑢) → (∀𝑢 ∈ 𝐴 𝑦 ∈ 𝑢 → ∀𝑢 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑢)) |
25 | 21, 24 | sylbir 238 |
. . . . . . . . 9
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ ∀𝑢 ∈ 𝐴 𝑥 ∈ 𝑢) → (∀𝑢 ∈ 𝐴 𝑦 ∈ 𝑢 → ∀𝑢 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑢)) |
26 | | vex 3403 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
27 | 26 | elint2 4844 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∩ 𝐴
↔ ∀𝑢 ∈
𝐴 𝑦 ∈ 𝑢) |
28 | | prex 5300 |
. . . . . . . . . 10
⊢ {𝑥, 𝑦} ∈ V |
29 | 28 | elint2 4844 |
. . . . . . . . 9
⊢ ({𝑥, 𝑦} ∈ ∩ 𝐴 ↔ ∀𝑢 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑢) |
30 | 25, 27, 29 | 3imtr4g 299 |
. . . . . . . 8
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ ∀𝑢 ∈ 𝐴 𝑥 ∈ 𝑢) → (𝑦 ∈ ∩ 𝐴 → {𝑥, 𝑦} ∈ ∩ 𝐴)) |
31 | 15, 30 | sylan2b 597 |
. . . . . . 7
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝑥 ∈ ∩ 𝐴) → (𝑦 ∈ ∩ 𝐴 → {𝑥, 𝑦} ∈ ∩ 𝐴)) |
32 | 31 | ralrimiv 3096 |
. . . . . 6
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝑥 ∈ ∩ 𝐴) → ∀𝑦 ∈ ∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴) |
33 | 32 | adantlr 715 |
. . . . 5
⊢
(((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴) → ∀𝑦 ∈ ∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴) |
34 | | elmapg 8453 |
. . . . . . . . . 10
⊢ ((∩ 𝐴
∈ V ∧ 𝑥 ∈ V)
→ (𝑦 ∈ (∩ 𝐴
↑m 𝑥)
↔ 𝑦:𝑥⟶∩ 𝐴)) |
35 | 34 | elvd 3406 |
. . . . . . . . 9
⊢ (∩ 𝐴
∈ V → (𝑦 ∈
(∩ 𝐴 ↑m 𝑥) ↔ 𝑦:𝑥⟶∩ 𝐴)) |
36 | 2, 35 | sylbi 220 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ → (𝑦 ∈ (∩ 𝐴
↑m 𝑥)
↔ 𝑦:𝑥⟶∩ 𝐴)) |
37 | 36 | ad2antlr 727 |
. . . . . . 7
⊢
(((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑦 ∈ (∩ 𝐴 ↑m 𝑥) ↔ 𝑦:𝑥⟶∩ 𝐴)) |
38 | | intss1 4852 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑢) |
39 | | fss 6522 |
. . . . . . . . . . . 12
⊢ ((𝑦:𝑥⟶∩ 𝐴 ∧ ∩ 𝐴
⊆ 𝑢) → 𝑦:𝑥⟶𝑢) |
40 | 38, 39 | sylan2 596 |
. . . . . . . . . . 11
⊢ ((𝑦:𝑥⟶∩ 𝐴 ∧ 𝑢 ∈ 𝐴) → 𝑦:𝑥⟶𝑢) |
41 | 40 | ralrimiva 3097 |
. . . . . . . . . 10
⊢ (𝑦:𝑥⟶∩ 𝐴 → ∀𝑢 ∈ 𝐴 𝑦:𝑥⟶𝑢) |
42 | | gruurn 10301 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ Univ ∧ 𝑥 ∈ 𝑢 ∧ 𝑦:𝑥⟶𝑢) → ∪ ran
𝑦 ∈ 𝑢) |
43 | 42 | 3expia 1122 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ Univ ∧ 𝑥 ∈ 𝑢) → (𝑦:𝑥⟶𝑢 → ∪ ran
𝑦 ∈ 𝑢)) |
44 | 43 | ral2imi 3072 |
. . . . . . . . . . . 12
⊢
(∀𝑢 ∈
𝐴 (𝑢 ∈ Univ ∧ 𝑥 ∈ 𝑢) → (∀𝑢 ∈ 𝐴 𝑦:𝑥⟶𝑢 → ∀𝑢 ∈ 𝐴 ∪ ran 𝑦 ∈ 𝑢)) |
45 | 21, 44 | sylbir 238 |
. . . . . . . . . . 11
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ ∀𝑢 ∈ 𝐴 𝑥 ∈ 𝑢) → (∀𝑢 ∈ 𝐴 𝑦:𝑥⟶𝑢 → ∀𝑢 ∈ 𝐴 ∪ ran 𝑦 ∈ 𝑢)) |
46 | 15, 45 | sylan2b 597 |
. . . . . . . . . 10
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝑥 ∈ ∩ 𝐴) → (∀𝑢 ∈ 𝐴 𝑦:𝑥⟶𝑢 → ∀𝑢 ∈ 𝐴 ∪ ran 𝑦 ∈ 𝑢)) |
47 | 41, 46 | syl5 34 |
. . . . . . . . 9
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝑥 ∈ ∩ 𝐴) → (𝑦:𝑥⟶∩ 𝐴 → ∀𝑢 ∈ 𝐴 ∪ ran 𝑦 ∈ 𝑢)) |
48 | 26 | rnex 7646 |
. . . . . . . . . . 11
⊢ ran 𝑦 ∈ V |
49 | 48 | uniex 7488 |
. . . . . . . . . 10
⊢ ∪ ran 𝑦 ∈ V |
50 | 49 | elint2 4844 |
. . . . . . . . 9
⊢ (∪ ran 𝑦 ∈ ∩ 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∪ ran 𝑦 ∈ 𝑢) |
51 | 47, 50 | syl6ibr 255 |
. . . . . . . 8
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝑥 ∈ ∩ 𝐴) → (𝑦:𝑥⟶∩ 𝐴 → ∪ ran 𝑦 ∈ ∩ 𝐴)) |
52 | 51 | adantlr 715 |
. . . . . . 7
⊢
(((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑦:𝑥⟶∩ 𝐴 → ∪ ran 𝑦 ∈ ∩ 𝐴)) |
53 | 37, 52 | sylbid 243 |
. . . . . 6
⊢
(((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑦 ∈ (∩ 𝐴 ↑m 𝑥) → ∪ ran 𝑦 ∈ ∩ 𝐴)) |
54 | 53 | ralrimiv 3096 |
. . . . 5
⊢
(((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴) → ∀𝑦 ∈ (∩ 𝐴
↑m 𝑥)∪ ran 𝑦 ∈ ∩ 𝐴) |
55 | 20, 33, 54 | 3jca 1129 |
. . . 4
⊢
(((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝐴) → (𝒫 𝑥 ∈ ∩ 𝐴
∧ ∀𝑦 ∈
∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴 ∧ ∀𝑦 ∈ (∩ 𝐴
↑m 𝑥)∪ ran 𝑦 ∈ ∩ 𝐴)) |
56 | 55 | ralrimiva 3097 |
. . 3
⊢
((∀𝑢 ∈
𝐴 𝑢 ∈ Univ ∧ 𝐴 ≠ ∅) → ∀𝑥 ∈ ∩ 𝐴(𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀𝑦 ∈ ∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴 ∧ ∀𝑦 ∈ (∩ 𝐴
↑m 𝑥)∪ ran 𝑦 ∈ ∩ 𝐴)) |
57 | 4, 56 | sylanb 584 |
. 2
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) →
∀𝑥 ∈ ∩ 𝐴(𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀𝑦 ∈ ∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴 ∧ ∀𝑦 ∈ (∩ 𝐴
↑m 𝑥)∪ ran 𝑦 ∈ ∩ 𝐴)) |
58 | | elgrug 10295 |
. . 3
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ Univ ↔ (Tr ∩ 𝐴
∧ ∀𝑥 ∈
∩ 𝐴(𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀𝑦 ∈ ∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴 ∧ ∀𝑦 ∈ (∩ 𝐴
↑m 𝑥)∪ ran 𝑦 ∈ ∩ 𝐴)))) |
59 | 58 | biimpar 481 |
. 2
⊢ ((∩ 𝐴
∈ V ∧ (Tr ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀𝑦 ∈ ∩ 𝐴{𝑥, 𝑦} ∈ ∩ 𝐴 ∧ ∀𝑦 ∈ (∩ 𝐴
↑m 𝑥)∪ ran 𝑦 ∈ ∩ 𝐴))) → ∩ 𝐴
∈ Univ) |
60 | 3, 10, 57, 59 | syl12anc 836 |
1
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ Univ) |