Step | Hyp | Ref
| Expression |
1 | | tsmsfbas.a |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝑊) |
2 | | elex 3450 |
. 2
⊢ (𝐴 ∈ 𝑊 → 𝐴 ∈ V) |
3 | | tsmsfbas.l |
. . 3
⊢ 𝐿 = ran 𝐹 |
4 | | ssrab2 4013 |
. . . . . . 7
⊢ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ⊆ 𝑆 |
5 | | tsmsfbas.s |
. . . . . . . . . 10
⊢ 𝑆 = (𝒫 𝐴 ∩ Fin) |
6 | | pwexg 5301 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V) |
7 | | inex1g 5243 |
. . . . . . . . . . 11
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
Fin) ∈ V) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝒫
𝐴 ∩ Fin) ∈
V) |
9 | 5, 8 | eqeltrid 2843 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → 𝑆 ∈ V) |
10 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → 𝑆 ∈ V) |
11 | | elpw2g 5268 |
. . . . . . . 8
⊢ (𝑆 ∈ V → ({𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ∈ 𝒫 𝑆 ↔ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ⊆ 𝑆)) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ({𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ∈ 𝒫 𝑆 ↔ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ⊆ 𝑆)) |
13 | 4, 12 | mpbiri 257 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ∈ 𝒫 𝑆) |
14 | | tsmsfbas.f |
. . . . . 6
⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
15 | 13, 14 | fmptd 6988 |
. . . . 5
⊢ (𝐴 ∈ V → 𝐹:𝑆⟶𝒫 𝑆) |
16 | 15 | frnd 6608 |
. . . 4
⊢ (𝐴 ∈ V → ran 𝐹 ⊆ 𝒫 𝑆) |
17 | | 0ss 4330 |
. . . . . . . . . 10
⊢ ∅
⊆ 𝐴 |
18 | | 0fin 8954 |
. . . . . . . . . 10
⊢ ∅
∈ Fin |
19 | | elfpw 9121 |
. . . . . . . . . 10
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin)) |
20 | 17, 18, 19 | mpbir2an 708 |
. . . . . . . . 9
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) |
21 | 20, 5 | eleqtrri 2838 |
. . . . . . . 8
⊢ ∅
∈ 𝑆 |
22 | | 0ss 4330 |
. . . . . . . . 9
⊢ ∅
⊆ 𝑦 |
23 | 22 | rgenw 3076 |
. . . . . . . 8
⊢
∀𝑦 ∈
𝑆 ∅ ⊆ 𝑦 |
24 | | rabid2 3314 |
. . . . . . . . . 10
⊢ (𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ↔ ∀𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) |
25 | | sseq1 3946 |
. . . . . . . . . . 11
⊢ (𝑧 = ∅ → (𝑧 ⊆ 𝑦 ↔ ∅ ⊆ 𝑦)) |
26 | 25 | ralbidv 3112 |
. . . . . . . . . 10
⊢ (𝑧 = ∅ → (∀𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ↔ ∀𝑦 ∈ 𝑆 ∅ ⊆ 𝑦)) |
27 | 24, 26 | bitrid 282 |
. . . . . . . . 9
⊢ (𝑧 = ∅ → (𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ↔ ∀𝑦 ∈ 𝑆 ∅ ⊆ 𝑦)) |
28 | 27 | rspcev 3561 |
. . . . . . . 8
⊢ ((∅
∈ 𝑆 ∧
∀𝑦 ∈ 𝑆 ∅ ⊆ 𝑦) → ∃𝑧 ∈ 𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
29 | 21, 23, 28 | mp2an 689 |
. . . . . . 7
⊢
∃𝑧 ∈
𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} |
30 | 14 | elrnmpt 5865 |
. . . . . . . 8
⊢ (𝑆 ∈ V → (𝑆 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) |
31 | 9, 30 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝑆 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) |
32 | 29, 31 | mpbiri 257 |
. . . . . 6
⊢ (𝐴 ∈ V → 𝑆 ∈ ran 𝐹) |
33 | 32 | ne0d 4269 |
. . . . 5
⊢ (𝐴 ∈ V → ran 𝐹 ≠ ∅) |
34 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
35 | | ssid 3943 |
. . . . . . . . . . . 12
⊢ 𝑧 ⊆ 𝑧 |
36 | | sseq2 3947 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ 𝑧)) |
37 | 36 | rspcev 3561 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑧 ⊆ 𝑧) → ∃𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) |
38 | 34, 35, 37 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) |
39 | | rabn0 4319 |
. . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) |
40 | 38, 39 | sylibr 233 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ≠ ∅) |
41 | 40 | necomd 2999 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ∅ ≠ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
42 | 41 | neneqd 2948 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ¬ ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
43 | 42 | nrexdv 3198 |
. . . . . . 7
⊢ (𝐴 ∈ V → ¬
∃𝑧 ∈ 𝑆 ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
44 | | 0ex 5231 |
. . . . . . . 8
⊢ ∅
∈ V |
45 | 14 | elrnmpt 5865 |
. . . . . . . 8
⊢ (∅
∈ V → (∅ ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑆 ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) |
46 | 44, 45 | ax-mp 5 |
. . . . . . 7
⊢ (∅
∈ ran 𝐹 ↔
∃𝑧 ∈ 𝑆 ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
47 | 43, 46 | sylnibr 329 |
. . . . . 6
⊢ (𝐴 ∈ V → ¬ ∅
∈ ran 𝐹) |
48 | | df-nel 3050 |
. . . . . 6
⊢ (∅
∉ ran 𝐹 ↔ ¬
∅ ∈ ran 𝐹) |
49 | 47, 48 | sylibr 233 |
. . . . 5
⊢ (𝐴 ∈ V → ∅ ∉
ran 𝐹) |
50 | | elfpw 9121 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑢 ⊆ 𝐴 ∧ 𝑢 ∈ Fin)) |
51 | 50 | simplbi 498 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (𝒫 𝐴 ∩ Fin) → 𝑢 ⊆ 𝐴) |
52 | 51, 5 | eleq2s 2857 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ 𝑆 → 𝑢 ⊆ 𝐴) |
53 | | elfpw 9121 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑣 ⊆ 𝐴 ∧ 𝑣 ∈ Fin)) |
54 | 53 | simplbi 498 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ (𝒫 𝐴 ∩ Fin) → 𝑣 ⊆ 𝐴) |
55 | 54, 5 | eleq2s 2857 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ 𝑆 → 𝑣 ⊆ 𝐴) |
56 | 52, 55 | anim12i 613 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴)) |
57 | | unss 4118 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴) ↔ (𝑢 ∪ 𝑣) ⊆ 𝐴) |
58 | 56, 57 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ∪ 𝑣) ⊆ 𝐴) |
59 | | elinel2 4130 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (𝒫 𝐴 ∩ Fin) → 𝑢 ∈ Fin) |
60 | 59, 5 | eleq2s 2857 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ Fin) |
61 | | elinel2 4130 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ (𝒫 𝐴 ∩ Fin) → 𝑣 ∈ Fin) |
62 | 61, 5 | eleq2s 2857 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ Fin) |
63 | | unfi 8955 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Fin ∧ 𝑣 ∈ Fin) → (𝑢 ∪ 𝑣) ∈ Fin) |
64 | 60, 62, 63 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ∪ 𝑣) ∈ Fin) |
65 | | elfpw 9121 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∪ 𝑣) ∈ (𝒫 𝐴 ∩ Fin) ↔ ((𝑢 ∪ 𝑣) ⊆ 𝐴 ∧ (𝑢 ∪ 𝑣) ∈ Fin)) |
66 | 58, 64, 65 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ∪ 𝑣) ∈ (𝒫 𝐴 ∩ Fin)) |
67 | 66 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢 ∪ 𝑣) ∈ (𝒫 𝐴 ∩ Fin)) |
68 | 67, 5 | eleqtrrdi 2850 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢 ∪ 𝑣) ∈ 𝑆) |
69 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
70 | | sseq1 3946 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝑢 ∪ 𝑣) → (𝑎 ⊆ 𝑦 ↔ (𝑢 ∪ 𝑣) ⊆ 𝑦)) |
71 | 70 | rabbidv 3414 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑢 ∪ 𝑣) → {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
72 | 71 | rspceeqv 3575 |
. . . . . . . . . . 11
⊢ (((𝑢 ∪ 𝑣) ∈ 𝑆 ∧ {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) → ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
73 | 68, 69, 72 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
74 | 9 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑆 ∈ V) |
75 | | rabexg 5255 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ V → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V) |
77 | | sseq1 3946 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑎 → (𝑧 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦)) |
78 | 77 | rabbidv 3414 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑎 → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
79 | 78 | cbvmptv 5187 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) = (𝑎 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
80 | 14, 79 | eqtri 2766 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑎 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
81 | 80 | elrnmpt 5865 |
. . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V → ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹 ↔ ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦})) |
82 | 76, 81 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹 ↔ ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦})) |
83 | 73, 82 | mpbird 256 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹) |
84 | | pwidg 4555 |
. . . . . . . . . 10
⊢ ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
85 | 76, 84 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
86 | | inelcm 4398 |
. . . . . . . . 9
⊢ (({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹 ∧ {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) → (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅) |
87 | 83, 85, 86 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅) |
88 | 87 | ralrimivva 3123 |
. . . . . . 7
⊢ (𝐴 ∈ V → ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅) |
89 | | rabexg 5255 |
. . . . . . . . . 10
⊢ (𝑆 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V) |
90 | 9, 89 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V) |
91 | 90 | ralrimivw 3104 |
. . . . . . . 8
⊢ (𝐴 ∈ V → ∀𝑢 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V) |
92 | | sseq1 3946 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑢 → (𝑧 ⊆ 𝑦 ↔ 𝑢 ⊆ 𝑦)) |
93 | 92 | rabbidv 3414 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑢 → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦}) |
94 | 93 | cbvmptv 5187 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) = (𝑢 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦}) |
95 | 14, 94 | eqtri 2766 |
. . . . . . . . 9
⊢ 𝐹 = (𝑢 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦}) |
96 | | ineq1 4139 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = ({𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) |
97 | | inrab 4240 |
. . . . . . . . . . . . . . 15
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = {𝑦 ∈ 𝑆 ∣ (𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦)} |
98 | | unss 4118 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦) ↔ (𝑢 ∪ 𝑣) ⊆ 𝑦) |
99 | 98 | rabbii 3408 |
. . . . . . . . . . . . . . 15
⊢ {𝑦 ∈ 𝑆 ∣ (𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦)} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} |
100 | 97, 99 | eqtri 2766 |
. . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} |
101 | 96, 100 | eqtrdi 2794 |
. . . . . . . . . . . . 13
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
102 | 101 | pweqd 4552 |
. . . . . . . . . . . 12
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
103 | 102 | ineq2d 4146 |
. . . . . . . . . . 11
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) = (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦})) |
104 | 103 | neeq1d 3003 |
. . . . . . . . . 10
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → ((ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) |
105 | 104 | ralbidv 3112 |
. . . . . . . . 9
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) |
106 | 95, 105 | ralrnmptw 6970 |
. . . . . . . 8
⊢
(∀𝑢 ∈
𝑆 {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V → (∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) |
107 | 91, 106 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ V → (∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) |
108 | 88, 107 | mpbird 256 |
. . . . . 6
⊢ (𝐴 ∈ V → ∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅) |
109 | | rabexg 5255 |
. . . . . . . . . 10
⊢ (𝑆 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V) |
110 | 9, 109 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V) |
111 | 110 | ralrimivw 3104 |
. . . . . . . 8
⊢ (𝐴 ∈ V → ∀𝑣 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V) |
112 | | sseq1 3946 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑣 → (𝑧 ⊆ 𝑦 ↔ 𝑣 ⊆ 𝑦)) |
113 | 112 | rabbidv 3414 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑣 → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) |
114 | 113 | cbvmptv 5187 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) = (𝑣 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) |
115 | 14, 114 | eqtri 2766 |
. . . . . . . . 9
⊢ 𝐹 = (𝑣 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) |
116 | | ineq2 4140 |
. . . . . . . . . . . 12
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → (𝑎 ∩ 𝑏) = (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) |
117 | 116 | pweqd 4552 |
. . . . . . . . . . 11
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → 𝒫 (𝑎 ∩ 𝑏) = 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) |
118 | 117 | ineq2d 4146 |
. . . . . . . . . 10
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → (ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) = (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}))) |
119 | 118 | neeq1d 3003 |
. . . . . . . . 9
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → ((ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) |
120 | 115, 119 | ralrnmptw 6970 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑆 {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V → (∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) |
121 | 111, 120 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ V → (∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) |
122 | 121 | ralbidv 3112 |
. . . . . 6
⊢ (𝐴 ∈ V → (∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ ∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) |
123 | 108, 122 | mpbird 256 |
. . . . 5
⊢ (𝐴 ∈ V → ∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅) |
124 | 33, 49, 123 | 3jca 1127 |
. . . 4
⊢ (𝐴 ∈ V → (ran 𝐹 ≠ ∅ ∧ ∅
∉ ran 𝐹 ∧
∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅)) |
125 | | isfbas 22980 |
. . . . 5
⊢ (𝑆 ∈ V → (ran 𝐹 ∈ (fBas‘𝑆) ↔ (ran 𝐹 ⊆ 𝒫 𝑆 ∧ (ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran
𝐹 ∧ ∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅)))) |
126 | 9, 125 | syl 17 |
. . . 4
⊢ (𝐴 ∈ V → (ran 𝐹 ∈ (fBas‘𝑆) ↔ (ran 𝐹 ⊆ 𝒫 𝑆 ∧ (ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran
𝐹 ∧ ∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅)))) |
127 | 16, 124, 126 | mpbir2and 710 |
. . 3
⊢ (𝐴 ∈ V → ran 𝐹 ∈ (fBas‘𝑆)) |
128 | 3, 127 | eqeltrid 2843 |
. 2
⊢ (𝐴 ∈ V → 𝐿 ∈ (fBas‘𝑆)) |
129 | 1, 2, 128 | 3syl 18 |
1
⊢ (𝜑 → 𝐿 ∈ (fBas‘𝑆)) |