Step | Hyp | Ref
| Expression |
1 | | tsmsfbas.a |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝑊) |
2 | | elex 3416 |
. 2
⊢ (𝐴 ∈ 𝑊 → 𝐴 ∈ V) |
3 | | tsmsfbas.l |
. . 3
⊢ 𝐿 = ran 𝐹 |
4 | | ssrab2 3969 |
. . . . . . 7
⊢ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ⊆ 𝑆 |
5 | | tsmsfbas.s |
. . . . . . . . . 10
⊢ 𝑆 = (𝒫 𝐴 ∩ Fin) |
6 | | pwexg 5245 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V) |
7 | | inex1g 5187 |
. . . . . . . . . . 11
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
Fin) ∈ V) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝒫
𝐴 ∩ Fin) ∈
V) |
9 | 5, 8 | eqeltrid 2837 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → 𝑆 ∈ V) |
10 | 9 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → 𝑆 ∈ V) |
11 | | elpw2g 5212 |
. . . . . . . 8
⊢ (𝑆 ∈ V → ({𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ∈ 𝒫 𝑆 ↔ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ⊆ 𝑆)) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ({𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ∈ 𝒫 𝑆 ↔ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ⊆ 𝑆)) |
13 | 4, 12 | mpbiri 261 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ∈ 𝒫 𝑆) |
14 | | tsmsfbas.f |
. . . . . 6
⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
15 | 13, 14 | fmptd 6888 |
. . . . 5
⊢ (𝐴 ∈ V → 𝐹:𝑆⟶𝒫 𝑆) |
16 | 15 | frnd 6512 |
. . . 4
⊢ (𝐴 ∈ V → ran 𝐹 ⊆ 𝒫 𝑆) |
17 | | 0ss 4285 |
. . . . . . . . . 10
⊢ ∅
⊆ 𝐴 |
18 | | 0fin 8770 |
. . . . . . . . . 10
⊢ ∅
∈ Fin |
19 | | elfpw 8899 |
. . . . . . . . . 10
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin)) |
20 | 17, 18, 19 | mpbir2an 711 |
. . . . . . . . 9
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) |
21 | 20, 5 | eleqtrri 2832 |
. . . . . . . 8
⊢ ∅
∈ 𝑆 |
22 | | 0ss 4285 |
. . . . . . . . 9
⊢ ∅
⊆ 𝑦 |
23 | 22 | rgenw 3065 |
. . . . . . . 8
⊢
∀𝑦 ∈
𝑆 ∅ ⊆ 𝑦 |
24 | | rabid2 3284 |
. . . . . . . . . 10
⊢ (𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ↔ ∀𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) |
25 | | sseq1 3902 |
. . . . . . . . . . 11
⊢ (𝑧 = ∅ → (𝑧 ⊆ 𝑦 ↔ ∅ ⊆ 𝑦)) |
26 | 25 | ralbidv 3109 |
. . . . . . . . . 10
⊢ (𝑧 = ∅ → (∀𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ↔ ∀𝑦 ∈ 𝑆 ∅ ⊆ 𝑦)) |
27 | 24, 26 | syl5bb 286 |
. . . . . . . . 9
⊢ (𝑧 = ∅ → (𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ↔ ∀𝑦 ∈ 𝑆 ∅ ⊆ 𝑦)) |
28 | 27 | rspcev 3526 |
. . . . . . . 8
⊢ ((∅
∈ 𝑆 ∧
∀𝑦 ∈ 𝑆 ∅ ⊆ 𝑦) → ∃𝑧 ∈ 𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
29 | 21, 23, 28 | mp2an 692 |
. . . . . . 7
⊢
∃𝑧 ∈
𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} |
30 | 14 | elrnmpt 5799 |
. . . . . . . 8
⊢ (𝑆 ∈ V → (𝑆 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) |
31 | 9, 30 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝑆 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) |
32 | 29, 31 | mpbiri 261 |
. . . . . 6
⊢ (𝐴 ∈ V → 𝑆 ∈ ran 𝐹) |
33 | 32 | ne0d 4224 |
. . . . 5
⊢ (𝐴 ∈ V → ran 𝐹 ≠ ∅) |
34 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
35 | | ssid 3899 |
. . . . . . . . . . . 12
⊢ 𝑧 ⊆ 𝑧 |
36 | | sseq2 3903 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ 𝑧)) |
37 | 36 | rspcev 3526 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑧 ⊆ 𝑧) → ∃𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) |
38 | 34, 35, 37 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) |
39 | | rabn0 4274 |
. . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) |
40 | 38, 39 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ≠ ∅) |
41 | 40 | necomd 2989 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ∅ ≠ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
42 | 41 | neneqd 2939 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ¬ ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
43 | 42 | nrexdv 3180 |
. . . . . . 7
⊢ (𝐴 ∈ V → ¬
∃𝑧 ∈ 𝑆 ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
44 | | 0ex 5175 |
. . . . . . . 8
⊢ ∅
∈ V |
45 | 14 | elrnmpt 5799 |
. . . . . . . 8
⊢ (∅
∈ V → (∅ ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑆 ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) |
46 | 44, 45 | ax-mp 5 |
. . . . . . 7
⊢ (∅
∈ ran 𝐹 ↔
∃𝑧 ∈ 𝑆 ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
47 | 43, 46 | sylnibr 332 |
. . . . . 6
⊢ (𝐴 ∈ V → ¬ ∅
∈ ran 𝐹) |
48 | | df-nel 3039 |
. . . . . 6
⊢ (∅
∉ ran 𝐹 ↔ ¬
∅ ∈ ran 𝐹) |
49 | 47, 48 | sylibr 237 |
. . . . 5
⊢ (𝐴 ∈ V → ∅ ∉
ran 𝐹) |
50 | | elfpw 8899 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑢 ⊆ 𝐴 ∧ 𝑢 ∈ Fin)) |
51 | 50 | simplbi 501 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (𝒫 𝐴 ∩ Fin) → 𝑢 ⊆ 𝐴) |
52 | 51, 5 | eleq2s 2851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ 𝑆 → 𝑢 ⊆ 𝐴) |
53 | | elfpw 8899 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑣 ⊆ 𝐴 ∧ 𝑣 ∈ Fin)) |
54 | 53 | simplbi 501 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ (𝒫 𝐴 ∩ Fin) → 𝑣 ⊆ 𝐴) |
55 | 54, 5 | eleq2s 2851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ 𝑆 → 𝑣 ⊆ 𝐴) |
56 | 52, 55 | anim12i 616 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴)) |
57 | | unss 4074 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴) ↔ (𝑢 ∪ 𝑣) ⊆ 𝐴) |
58 | 56, 57 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ∪ 𝑣) ⊆ 𝐴) |
59 | | elinel2 4086 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (𝒫 𝐴 ∩ Fin) → 𝑢 ∈ Fin) |
60 | 59, 5 | eleq2s 2851 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ Fin) |
61 | | elinel2 4086 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ (𝒫 𝐴 ∩ Fin) → 𝑣 ∈ Fin) |
62 | 61, 5 | eleq2s 2851 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ Fin) |
63 | | unfi 8771 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Fin ∧ 𝑣 ∈ Fin) → (𝑢 ∪ 𝑣) ∈ Fin) |
64 | 60, 62, 63 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ∪ 𝑣) ∈ Fin) |
65 | | elfpw 8899 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∪ 𝑣) ∈ (𝒫 𝐴 ∩ Fin) ↔ ((𝑢 ∪ 𝑣) ⊆ 𝐴 ∧ (𝑢 ∪ 𝑣) ∈ Fin)) |
66 | 58, 64, 65 | sylanbrc 586 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ∪ 𝑣) ∈ (𝒫 𝐴 ∩ Fin)) |
67 | 66 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢 ∪ 𝑣) ∈ (𝒫 𝐴 ∩ Fin)) |
68 | 67, 5 | eleqtrrdi 2844 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢 ∪ 𝑣) ∈ 𝑆) |
69 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
70 | | sseq1 3902 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝑢 ∪ 𝑣) → (𝑎 ⊆ 𝑦 ↔ (𝑢 ∪ 𝑣) ⊆ 𝑦)) |
71 | 70 | rabbidv 3381 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑢 ∪ 𝑣) → {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
72 | 71 | rspceeqv 3541 |
. . . . . . . . . . 11
⊢ (((𝑢 ∪ 𝑣) ∈ 𝑆 ∧ {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) → ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
73 | 68, 69, 72 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
74 | 9 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑆 ∈ V) |
75 | | rabexg 5199 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ V → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V) |
77 | | sseq1 3902 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑎 → (𝑧 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦)) |
78 | 77 | rabbidv 3381 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑎 → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
79 | 78 | cbvmptv 5133 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) = (𝑎 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
80 | 14, 79 | eqtri 2761 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑎 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) |
81 | 80 | elrnmpt 5799 |
. . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V → ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹 ↔ ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦})) |
82 | 76, 81 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹 ↔ ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦})) |
83 | 73, 82 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹) |
84 | | pwidg 4510 |
. . . . . . . . . 10
⊢ ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
85 | 76, 84 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
86 | | inelcm 4354 |
. . . . . . . . 9
⊢ (({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹 ∧ {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) → (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅) |
87 | 83, 85, 86 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅) |
88 | 87 | ralrimivva 3103 |
. . . . . . 7
⊢ (𝐴 ∈ V → ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅) |
89 | | rabexg 5199 |
. . . . . . . . . 10
⊢ (𝑆 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V) |
90 | 9, 89 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V) |
91 | 90 | ralrimivw 3097 |
. . . . . . . 8
⊢ (𝐴 ∈ V → ∀𝑢 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V) |
92 | | sseq1 3902 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑢 → (𝑧 ⊆ 𝑦 ↔ 𝑢 ⊆ 𝑦)) |
93 | 92 | rabbidv 3381 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑢 → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦}) |
94 | 93 | cbvmptv 5133 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) = (𝑢 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦}) |
95 | 14, 94 | eqtri 2761 |
. . . . . . . . 9
⊢ 𝐹 = (𝑢 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦}) |
96 | | ineq1 4096 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = ({𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) |
97 | | inrab 4195 |
. . . . . . . . . . . . . . 15
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = {𝑦 ∈ 𝑆 ∣ (𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦)} |
98 | | unss 4074 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦) ↔ (𝑢 ∪ 𝑣) ⊆ 𝑦) |
99 | 98 | rabbii 3374 |
. . . . . . . . . . . . . . 15
⊢ {𝑦 ∈ 𝑆 ∣ (𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦)} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} |
100 | 97, 99 | eqtri 2761 |
. . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} |
101 | 96, 100 | eqtrdi 2789 |
. . . . . . . . . . . . 13
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
102 | 101 | pweqd 4507 |
. . . . . . . . . . . 12
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) |
103 | 102 | ineq2d 4103 |
. . . . . . . . . . 11
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) = (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦})) |
104 | 103 | neeq1d 2993 |
. . . . . . . . . 10
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → ((ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) |
105 | 104 | ralbidv 3109 |
. . . . . . . . 9
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) |
106 | 95, 105 | ralrnmptw 6870 |
. . . . . . . 8
⊢
(∀𝑢 ∈
𝑆 {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V → (∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) |
107 | 91, 106 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ V → (∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) |
108 | 88, 107 | mpbird 260 |
. . . . . 6
⊢ (𝐴 ∈ V → ∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅) |
109 | | rabexg 5199 |
. . . . . . . . . 10
⊢ (𝑆 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V) |
110 | 9, 109 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V) |
111 | 110 | ralrimivw 3097 |
. . . . . . . 8
⊢ (𝐴 ∈ V → ∀𝑣 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V) |
112 | | sseq1 3902 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑣 → (𝑧 ⊆ 𝑦 ↔ 𝑣 ⊆ 𝑦)) |
113 | 112 | rabbidv 3381 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑣 → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) |
114 | 113 | cbvmptv 5133 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) = (𝑣 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) |
115 | 14, 114 | eqtri 2761 |
. . . . . . . . 9
⊢ 𝐹 = (𝑣 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) |
116 | | ineq2 4097 |
. . . . . . . . . . . 12
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → (𝑎 ∩ 𝑏) = (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) |
117 | 116 | pweqd 4507 |
. . . . . . . . . . 11
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → 𝒫 (𝑎 ∩ 𝑏) = 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) |
118 | 117 | ineq2d 4103 |
. . . . . . . . . 10
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → (ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) = (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}))) |
119 | 118 | neeq1d 2993 |
. . . . . . . . 9
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → ((ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) |
120 | 115, 119 | ralrnmptw 6870 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑆 {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V → (∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) |
121 | 111, 120 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ V → (∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) |
122 | 121 | ralbidv 3109 |
. . . . . 6
⊢ (𝐴 ∈ V → (∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ ∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) |
123 | 108, 122 | mpbird 260 |
. . . . 5
⊢ (𝐴 ∈ V → ∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅) |
124 | 33, 49, 123 | 3jca 1129 |
. . . 4
⊢ (𝐴 ∈ V → (ran 𝐹 ≠ ∅ ∧ ∅
∉ ran 𝐹 ∧
∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅)) |
125 | | isfbas 22580 |
. . . . 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 713 |
. . 3
⊢ (𝐴 ∈ V → ran 𝐹 ∈ (fBas‘𝑆)) |
128 | 3, 127 | eqeltrid 2837 |
. 2
⊢ (𝐴 ∈ V → 𝐿 ∈ (fBas‘𝑆)) |
129 | 1, 2, 128 | 3syl 18 |
1
⊢ (𝜑 → 𝐿 ∈ (fBas‘𝑆)) |