| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tsmsfbas.a | . 2
⊢ (𝜑 → 𝐴 ∈ 𝑊) | 
| 2 |  | elex 3501 | . 2
⊢ (𝐴 ∈ 𝑊 → 𝐴 ∈ V) | 
| 3 |  | tsmsfbas.l | . . 3
⊢ 𝐿 = ran 𝐹 | 
| 4 |  | ssrab2 4080 | . . . . . . 7
⊢ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ⊆ 𝑆 | 
| 5 |  | tsmsfbas.s | . . . . . . . . . 10
⊢ 𝑆 = (𝒫 𝐴 ∩ Fin) | 
| 6 |  | pwexg 5378 | . . . . . . . . . . 11
⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V) | 
| 7 |  | inex1g 5319 | . . . . . . . . . . 11
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
Fin) ∈ V) | 
| 8 | 6, 7 | syl 17 | . . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝒫
𝐴 ∩ Fin) ∈
V) | 
| 9 | 5, 8 | eqeltrid 2845 | . . . . . . . . 9
⊢ (𝐴 ∈ V → 𝑆 ∈ V) | 
| 10 | 9 | adantr 480 | . . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → 𝑆 ∈ V) | 
| 11 |  | elpw2g 5333 | . . . . . . . 8
⊢ (𝑆 ∈ V → ({𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ∈ 𝒫 𝑆 ↔ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ⊆ 𝑆)) | 
| 12 | 10, 11 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ({𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ∈ 𝒫 𝑆 ↔ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ⊆ 𝑆)) | 
| 13 | 4, 12 | mpbiri 258 | . . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ∈ 𝒫 𝑆) | 
| 14 |  | tsmsfbas.f | . . . . . 6
⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) | 
| 15 | 13, 14 | fmptd 7134 | . . . . 5
⊢ (𝐴 ∈ V → 𝐹:𝑆⟶𝒫 𝑆) | 
| 16 | 15 | frnd 6744 | . . . 4
⊢ (𝐴 ∈ V → ran 𝐹 ⊆ 𝒫 𝑆) | 
| 17 |  | 0ss 4400 | . . . . . . . . . 10
⊢ ∅
⊆ 𝐴 | 
| 18 |  | 0fi 9082 | . . . . . . . . . 10
⊢ ∅
∈ Fin | 
| 19 |  | elfpw 9394 | . . . . . . . . . 10
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin)) | 
| 20 | 17, 18, 19 | mpbir2an 711 | . . . . . . . . 9
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) | 
| 21 | 20, 5 | eleqtrri 2840 | . . . . . . . 8
⊢ ∅
∈ 𝑆 | 
| 22 |  | 0ss 4400 | . . . . . . . . 9
⊢ ∅
⊆ 𝑦 | 
| 23 | 22 | rgenw 3065 | . . . . . . . 8
⊢
∀𝑦 ∈
𝑆 ∅ ⊆ 𝑦 | 
| 24 |  | rabid2 3470 | . . . . . . . . . 10
⊢ (𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ↔ ∀𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) | 
| 25 |  | sseq1 4009 | . . . . . . . . . . 11
⊢ (𝑧 = ∅ → (𝑧 ⊆ 𝑦 ↔ ∅ ⊆ 𝑦)) | 
| 26 | 25 | ralbidv 3178 | . . . . . . . . . 10
⊢ (𝑧 = ∅ → (∀𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ↔ ∀𝑦 ∈ 𝑆 ∅ ⊆ 𝑦)) | 
| 27 | 24, 26 | bitrid 283 | . . . . . . . . 9
⊢ (𝑧 = ∅ → (𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ↔ ∀𝑦 ∈ 𝑆 ∅ ⊆ 𝑦)) | 
| 28 | 27 | rspcev 3622 | . . . . . . . 8
⊢ ((∅
∈ 𝑆 ∧
∀𝑦 ∈ 𝑆 ∅ ⊆ 𝑦) → ∃𝑧 ∈ 𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) | 
| 29 | 21, 23, 28 | mp2an 692 | . . . . . . 7
⊢
∃𝑧 ∈
𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} | 
| 30 | 14 | elrnmpt 5969 | . . . . . . . 8
⊢ (𝑆 ∈ V → (𝑆 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) | 
| 31 | 9, 30 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ V → (𝑆 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑆 𝑆 = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) | 
| 32 | 29, 31 | mpbiri 258 | . . . . . 6
⊢ (𝐴 ∈ V → 𝑆 ∈ ran 𝐹) | 
| 33 | 32 | ne0d 4342 | . . . . 5
⊢ (𝐴 ∈ V → ran 𝐹 ≠ ∅) | 
| 34 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) | 
| 35 |  | ssid 4006 | . . . . . . . . . . . 12
⊢ 𝑧 ⊆ 𝑧 | 
| 36 |  | sseq2 4010 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ 𝑧)) | 
| 37 | 36 | rspcev 3622 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑧 ⊆ 𝑧) → ∃𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) | 
| 38 | 34, 35, 37 | sylancl 586 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) | 
| 39 |  | rabn0 4389 | . . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦) | 
| 40 | 38, 39 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} ≠ ∅) | 
| 41 | 40 | necomd 2996 | . . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ∅ ≠ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) | 
| 42 | 41 | neneqd 2945 | . . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝑆) → ¬ ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) | 
| 43 | 42 | nrexdv 3149 | . . . . . . 7
⊢ (𝐴 ∈ V → ¬
∃𝑧 ∈ 𝑆 ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) | 
| 44 |  | 0ex 5307 | . . . . . . . 8
⊢ ∅
∈ V | 
| 45 | 14 | elrnmpt 5969 | . . . . . . . 8
⊢ (∅
∈ V → (∅ ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑆 ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) | 
| 46 | 44, 45 | ax-mp 5 | . . . . . . 7
⊢ (∅
∈ ran 𝐹 ↔
∃𝑧 ∈ 𝑆 ∅ = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) | 
| 47 | 43, 46 | sylnibr 329 | . . . . . 6
⊢ (𝐴 ∈ V → ¬ ∅
∈ ran 𝐹) | 
| 48 |  | df-nel 3047 | . . . . . 6
⊢ (∅
∉ ran 𝐹 ↔ ¬
∅ ∈ ran 𝐹) | 
| 49 | 47, 48 | sylibr 234 | . . . . 5
⊢ (𝐴 ∈ V → ∅ ∉
ran 𝐹) | 
| 50 |  | elfpw 9394 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑢 ⊆ 𝐴 ∧ 𝑢 ∈ Fin)) | 
| 51 | 50 | simplbi 497 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (𝒫 𝐴 ∩ Fin) → 𝑢 ⊆ 𝐴) | 
| 52 | 51, 5 | eleq2s 2859 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ 𝑆 → 𝑢 ⊆ 𝐴) | 
| 53 |  | elfpw 9394 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑣 ⊆ 𝐴 ∧ 𝑣 ∈ Fin)) | 
| 54 | 53 | simplbi 497 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ (𝒫 𝐴 ∩ Fin) → 𝑣 ⊆ 𝐴) | 
| 55 | 54, 5 | eleq2s 2859 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ 𝑆 → 𝑣 ⊆ 𝐴) | 
| 56 | 52, 55 | anim12i 613 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴)) | 
| 57 |  | unss 4190 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴) ↔ (𝑢 ∪ 𝑣) ⊆ 𝐴) | 
| 58 | 56, 57 | sylib 218 | . . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ∪ 𝑣) ⊆ 𝐴) | 
| 59 |  | elinel2 4202 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (𝒫 𝐴 ∩ Fin) → 𝑢 ∈ Fin) | 
| 60 | 59, 5 | eleq2s 2859 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ Fin) | 
| 61 |  | elinel2 4202 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ (𝒫 𝐴 ∩ Fin) → 𝑣 ∈ Fin) | 
| 62 | 61, 5 | eleq2s 2859 | . . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ Fin) | 
| 63 |  | unfi 9211 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Fin ∧ 𝑣 ∈ Fin) → (𝑢 ∪ 𝑣) ∈ Fin) | 
| 64 | 60, 62, 63 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ∪ 𝑣) ∈ Fin) | 
| 65 |  | elfpw 9394 | . . . . . . . . . . . . . 14
⊢ ((𝑢 ∪ 𝑣) ∈ (𝒫 𝐴 ∩ Fin) ↔ ((𝑢 ∪ 𝑣) ⊆ 𝐴 ∧ (𝑢 ∪ 𝑣) ∈ Fin)) | 
| 66 | 58, 64, 65 | sylanbrc 583 | . . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 ∪ 𝑣) ∈ (𝒫 𝐴 ∩ Fin)) | 
| 67 | 66 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢 ∪ 𝑣) ∈ (𝒫 𝐴 ∩ Fin)) | 
| 68 | 67, 5 | eleqtrrdi 2852 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (𝑢 ∪ 𝑣) ∈ 𝑆) | 
| 69 |  | eqidd 2738 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) | 
| 70 |  | sseq1 4009 | . . . . . . . . . . . . 13
⊢ (𝑎 = (𝑢 ∪ 𝑣) → (𝑎 ⊆ 𝑦 ↔ (𝑢 ∪ 𝑣) ⊆ 𝑦)) | 
| 71 | 70 | rabbidv 3444 | . . . . . . . . . . . 12
⊢ (𝑎 = (𝑢 ∪ 𝑣) → {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) | 
| 72 | 71 | rspceeqv 3645 | . . . . . . . . . . 11
⊢ (((𝑢 ∪ 𝑣) ∈ 𝑆 ∧ {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) → ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) | 
| 73 | 68, 69, 72 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) | 
| 74 | 9 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → 𝑆 ∈ V) | 
| 75 |  | rabexg 5337 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ V → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V) | 
| 76 | 74, 75 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V) | 
| 77 |  | sseq1 4009 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑎 → (𝑧 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦)) | 
| 78 | 77 | rabbidv 3444 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑎 → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) | 
| 79 | 78 | cbvmptv 5255 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) = (𝑎 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) | 
| 80 | 14, 79 | eqtri 2765 | . . . . . . . . . . . 12
⊢ 𝐹 = (𝑎 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦}) | 
| 81 | 80 | elrnmpt 5969 | . . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V → ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹 ↔ ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦})) | 
| 82 | 76, 81 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹 ↔ ∃𝑎 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦})) | 
| 83 | 73, 82 | mpbird 257 | . . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹) | 
| 84 |  | pwidg 4620 | . . . . . . . . . 10
⊢ ({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ V → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) | 
| 85 | 76, 84 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) | 
| 86 |  | inelcm 4465 | . . . . . . . . 9
⊢ (({𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ ran 𝐹 ∧ {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) → (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅) | 
| 87 | 83, 85, 86 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ V ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅) | 
| 88 | 87 | ralrimivva 3202 | . . . . . . 7
⊢ (𝐴 ∈ V → ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅) | 
| 89 |  | rabexg 5337 | . . . . . . . . . 10
⊢ (𝑆 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V) | 
| 90 | 9, 89 | syl 17 | . . . . . . . . 9
⊢ (𝐴 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V) | 
| 91 | 90 | ralrimivw 3150 | . . . . . . . 8
⊢ (𝐴 ∈ V → ∀𝑢 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V) | 
| 92 |  | sseq1 4009 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑢 → (𝑧 ⊆ 𝑦 ↔ 𝑢 ⊆ 𝑦)) | 
| 93 | 92 | rabbidv 3444 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑢 → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦}) | 
| 94 | 93 | cbvmptv 5255 | . . . . . . . . . 10
⊢ (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) = (𝑢 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦}) | 
| 95 | 14, 94 | eqtri 2765 | . . . . . . . . 9
⊢ 𝐹 = (𝑢 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦}) | 
| 96 |  | ineq1 4213 | . . . . . . . . . . . . . 14
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = ({𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) | 
| 97 |  | inrab 4316 | . . . . . . . . . . . . . . 15
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = {𝑦 ∈ 𝑆 ∣ (𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦)} | 
| 98 |  | unss 4190 | . . . . . . . . . . . . . . . 16
⊢ ((𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦) ↔ (𝑢 ∪ 𝑣) ⊆ 𝑦) | 
| 99 | 98 | rabbii 3442 | . . . . . . . . . . . . . . 15
⊢ {𝑦 ∈ 𝑆 ∣ (𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦)} = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} | 
| 100 | 97, 99 | eqtri 2765 | . . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦} | 
| 101 | 96, 100 | eqtrdi 2793 | . . . . . . . . . . . . 13
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) | 
| 102 | 101 | pweqd 4617 | . . . . . . . . . . . 12
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) = 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) | 
| 103 | 102 | ineq2d 4220 | . . . . . . . . . . 11
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) = (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦})) | 
| 104 | 103 | neeq1d 3000 | . . . . . . . . . 10
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → ((ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) | 
| 105 | 104 | ralbidv 3178 | . . . . . . . . 9
⊢ (𝑎 = {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} → (∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) | 
| 106 | 95, 105 | ralrnmptw 7114 | . . . . . . . 8
⊢
(∀𝑢 ∈
𝑆 {𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦} ∈ V → (∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) | 
| 107 | 91, 106 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ V → (∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅ ↔ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 {𝑦 ∈ 𝑆 ∣ (𝑢 ∪ 𝑣) ⊆ 𝑦}) ≠ ∅)) | 
| 108 | 88, 107 | mpbird 257 | . . . . . 6
⊢ (𝐴 ∈ V → ∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅) | 
| 109 |  | rabexg 5337 | . . . . . . . . . 10
⊢ (𝑆 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V) | 
| 110 | 9, 109 | syl 17 | . . . . . . . . 9
⊢ (𝐴 ∈ V → {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V) | 
| 111 | 110 | ralrimivw 3150 | . . . . . . . 8
⊢ (𝐴 ∈ V → ∀𝑣 ∈ 𝑆 {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V) | 
| 112 |  | sseq1 4009 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑣 → (𝑧 ⊆ 𝑦 ↔ 𝑣 ⊆ 𝑦)) | 
| 113 | 112 | rabbidv 3444 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑣 → {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) | 
| 114 | 113 | cbvmptv 5255 | . . . . . . . . . 10
⊢ (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) = (𝑣 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) | 
| 115 | 14, 114 | eqtri 2765 | . . . . . . . . 9
⊢ 𝐹 = (𝑣 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}) | 
| 116 |  | ineq2 4214 | . . . . . . . . . . . 12
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → (𝑎 ∩ 𝑏) = (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) | 
| 117 | 116 | pweqd 4617 | . . . . . . . . . . 11
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → 𝒫 (𝑎 ∩ 𝑏) = 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) | 
| 118 | 117 | ineq2d 4220 | . . . . . . . . . 10
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → (ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) = (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦}))) | 
| 119 | 118 | neeq1d 3000 | . . . . . . . . 9
⊢ (𝑏 = {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} → ((ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) | 
| 120 | 115, 119 | ralrnmptw 7114 | . . . . . . . 8
⊢
(∀𝑣 ∈
𝑆 {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦} ∈ V → (∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) | 
| 121 | 111, 120 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ V → (∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ ∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) | 
| 122 | 121 | ralbidv 3178 | . . . . . 6
⊢ (𝐴 ∈ V → (∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅ ↔ ∀𝑎 ∈ ran 𝐹∀𝑣 ∈ 𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦})) ≠ ∅)) | 
| 123 | 108, 122 | mpbird 257 | . . . . 5
⊢ (𝐴 ∈ V → ∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅) | 
| 124 | 33, 49, 123 | 3jca 1129 | . . . 4
⊢ (𝐴 ∈ V → (ran 𝐹 ≠ ∅ ∧ ∅
∉ ran 𝐹 ∧
∀𝑎 ∈ ran 𝐹∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎 ∩ 𝑏)) ≠ ∅)) | 
| 125 |  | isfbas 23837 | . . . . 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 2845 | . 2
⊢ (𝐴 ∈ V → 𝐿 ∈ (fBas‘𝑆)) | 
| 129 | 1, 2, 128 | 3syl 18 | 1
⊢ (𝜑 → 𝐿 ∈ (fBas‘𝑆)) |