Step |
Hyp |
Ref |
Expression |
1 |
|
tsmsfbas.s |
⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin ) |
2 |
|
tsmsfbas.f |
⊢ 𝐹 = ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) |
3 |
|
tsmsfbas.l |
⊢ 𝐿 = ran 𝐹 |
4 |
|
tsmsfbas.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑊 ) |
5 |
|
elex |
⊢ ( 𝐴 ∈ 𝑊 → 𝐴 ∈ V ) |
6 |
|
ssrab2 |
⊢ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ 𝑆 |
7 |
|
pwexg |
⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V ) |
8 |
|
inex1g |
⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∩ Fin ) ∈ V ) |
9 |
7 8
|
syl |
⊢ ( 𝐴 ∈ V → ( 𝒫 𝐴 ∩ Fin ) ∈ V ) |
10 |
1 9
|
eqeltrid |
⊢ ( 𝐴 ∈ V → 𝑆 ∈ V ) |
11 |
10
|
adantr |
⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → 𝑆 ∈ V ) |
12 |
|
elpw2g |
⊢ ( 𝑆 ∈ V → ( { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ 𝒫 𝑆 ↔ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ 𝑆 ) ) |
13 |
11 12
|
syl |
⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → ( { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ 𝒫 𝑆 ↔ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ 𝑆 ) ) |
14 |
6 13
|
mpbiri |
⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ 𝒫 𝑆 ) |
15 |
14 2
|
fmptd |
⊢ ( 𝐴 ∈ V → 𝐹 : 𝑆 ⟶ 𝒫 𝑆 ) |
16 |
15
|
frnd |
⊢ ( 𝐴 ∈ V → ran 𝐹 ⊆ 𝒫 𝑆 ) |
17 |
|
0ss |
⊢ ∅ ⊆ 𝐴 |
18 |
|
0fin |
⊢ ∅ ∈ Fin |
19 |
|
elfpw |
⊢ ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ∅ ⊆ 𝐴 ∧ ∅ ∈ Fin ) ) |
20 |
17 18 19
|
mpbir2an |
⊢ ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) |
21 |
20 1
|
eleqtrri |
⊢ ∅ ∈ 𝑆 |
22 |
|
0ss |
⊢ ∅ ⊆ 𝑦 |
23 |
22
|
rgenw |
⊢ ∀ 𝑦 ∈ 𝑆 ∅ ⊆ 𝑦 |
24 |
|
rabid2 |
⊢ ( 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ↔ ∀ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ) |
25 |
|
sseq1 |
⊢ ( 𝑧 = ∅ → ( 𝑧 ⊆ 𝑦 ↔ ∅ ⊆ 𝑦 ) ) |
26 |
25
|
ralbidv |
⊢ ( 𝑧 = ∅ → ( ∀ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 ∅ ⊆ 𝑦 ) ) |
27 |
24 26
|
syl5bb |
⊢ ( 𝑧 = ∅ → ( 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ↔ ∀ 𝑦 ∈ 𝑆 ∅ ⊆ 𝑦 ) ) |
28 |
27
|
rspcev |
⊢ ( ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ∅ ⊆ 𝑦 ) → ∃ 𝑧 ∈ 𝑆 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) |
29 |
21 23 28
|
mp2an |
⊢ ∃ 𝑧 ∈ 𝑆 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } |
30 |
2
|
elrnmpt |
⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑆 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ) |
31 |
10 30
|
syl |
⊢ ( 𝐴 ∈ V → ( 𝑆 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑆 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ) |
32 |
29 31
|
mpbiri |
⊢ ( 𝐴 ∈ V → 𝑆 ∈ ran 𝐹 ) |
33 |
32
|
ne0d |
⊢ ( 𝐴 ∈ V → ran 𝐹 ≠ ∅ ) |
34 |
|
simpr |
⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 ) |
35 |
|
ssid |
⊢ 𝑧 ⊆ 𝑧 |
36 |
|
sseq2 |
⊢ ( 𝑦 = 𝑧 → ( 𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ 𝑧 ) ) |
37 |
36
|
rspcev |
⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑧 ⊆ 𝑧 ) → ∃ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ) |
38 |
34 35 37
|
sylancl |
⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → ∃ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ) |
39 |
|
rabn0 |
⊢ ( { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ) |
40 |
38 39
|
sylibr |
⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ≠ ∅ ) |
41 |
40
|
necomd |
⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → ∅ ≠ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) |
42 |
41
|
neneqd |
⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → ¬ ∅ = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) |
43 |
42
|
nrexdv |
⊢ ( 𝐴 ∈ V → ¬ ∃ 𝑧 ∈ 𝑆 ∅ = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) |
44 |
|
0ex |
⊢ ∅ ∈ V |
45 |
2
|
elrnmpt |
⊢ ( ∅ ∈ V → ( ∅ ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑆 ∅ = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ) |
46 |
44 45
|
ax-mp |
⊢ ( ∅ ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑆 ∅ = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) |
47 |
43 46
|
sylnibr |
⊢ ( 𝐴 ∈ V → ¬ ∅ ∈ ran 𝐹 ) |
48 |
|
df-nel |
⊢ ( ∅ ∉ ran 𝐹 ↔ ¬ ∅ ∈ ran 𝐹 ) |
49 |
47 48
|
sylibr |
⊢ ( 𝐴 ∈ V → ∅ ∉ ran 𝐹 ) |
50 |
|
elfpw |
⊢ ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑢 ⊆ 𝐴 ∧ 𝑢 ∈ Fin ) ) |
51 |
50
|
simplbi |
⊢ ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑢 ⊆ 𝐴 ) |
52 |
51 1
|
eleq2s |
⊢ ( 𝑢 ∈ 𝑆 → 𝑢 ⊆ 𝐴 ) |
53 |
|
elfpw |
⊢ ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑣 ⊆ 𝐴 ∧ 𝑣 ∈ Fin ) ) |
54 |
53
|
simplbi |
⊢ ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑣 ⊆ 𝐴 ) |
55 |
54 1
|
eleq2s |
⊢ ( 𝑣 ∈ 𝑆 → 𝑣 ⊆ 𝐴 ) |
56 |
52 55
|
anim12i |
⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴 ) ) |
57 |
|
unss |
⊢ ( ( 𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴 ) ↔ ( 𝑢 ∪ 𝑣 ) ⊆ 𝐴 ) |
58 |
56 57
|
sylib |
⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ∪ 𝑣 ) ⊆ 𝐴 ) |
59 |
|
elinel2 |
⊢ ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑢 ∈ Fin ) |
60 |
59 1
|
eleq2s |
⊢ ( 𝑢 ∈ 𝑆 → 𝑢 ∈ Fin ) |
61 |
|
elinel2 |
⊢ ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑣 ∈ Fin ) |
62 |
61 1
|
eleq2s |
⊢ ( 𝑣 ∈ 𝑆 → 𝑣 ∈ Fin ) |
63 |
|
unfi |
⊢ ( ( 𝑢 ∈ Fin ∧ 𝑣 ∈ Fin ) → ( 𝑢 ∪ 𝑣 ) ∈ Fin ) |
64 |
60 62 63
|
syl2an |
⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ∪ 𝑣 ) ∈ Fin ) |
65 |
|
elfpw |
⊢ ( ( 𝑢 ∪ 𝑣 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ( 𝑢 ∪ 𝑣 ) ⊆ 𝐴 ∧ ( 𝑢 ∪ 𝑣 ) ∈ Fin ) ) |
66 |
58 64 65
|
sylanbrc |
⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ∪ 𝑣 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
67 |
66
|
adantl |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( 𝑢 ∪ 𝑣 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
68 |
67 1
|
eleqtrrdi |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ) |
69 |
|
eqidd |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) |
70 |
|
sseq1 |
⊢ ( 𝑎 = ( 𝑢 ∪ 𝑣 ) → ( 𝑎 ⊆ 𝑦 ↔ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 ) ) |
71 |
70
|
rabbidv |
⊢ ( 𝑎 = ( 𝑢 ∪ 𝑣 ) → { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) |
72 |
71
|
rspceeqv |
⊢ ( ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) → ∃ 𝑎 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } ) |
73 |
68 69 72
|
syl2anc |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ∃ 𝑎 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } ) |
74 |
10
|
adantr |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → 𝑆 ∈ V ) |
75 |
|
rabexg |
⊢ ( 𝑆 ∈ V → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ V ) |
76 |
74 75
|
syl |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ V ) |
77 |
|
sseq1 |
⊢ ( 𝑧 = 𝑎 → ( 𝑧 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦 ) ) |
78 |
77
|
rabbidv |
⊢ ( 𝑧 = 𝑎 → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } ) |
79 |
78
|
cbvmptv |
⊢ ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) = ( 𝑎 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } ) |
80 |
2 79
|
eqtri |
⊢ 𝐹 = ( 𝑎 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } ) |
81 |
80
|
elrnmpt |
⊢ ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ V → ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ ran 𝐹 ↔ ∃ 𝑎 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } ) ) |
82 |
76 81
|
syl |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ ran 𝐹 ↔ ∃ 𝑎 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } ) ) |
83 |
73 82
|
mpbird |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ ran 𝐹 ) |
84 |
|
pwidg |
⊢ ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ V → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) |
85 |
76 84
|
syl |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) |
86 |
|
inelcm |
⊢ ( ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ ran 𝐹 ∧ { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) → ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) |
87 |
83 85 86
|
syl2anc |
⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) |
88 |
87
|
ralrimivva |
⊢ ( 𝐴 ∈ V → ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) |
89 |
|
rabexg |
⊢ ( 𝑆 ∈ V → { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∈ V ) |
90 |
10 89
|
syl |
⊢ ( 𝐴 ∈ V → { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∈ V ) |
91 |
90
|
ralrimivw |
⊢ ( 𝐴 ∈ V → ∀ 𝑢 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∈ V ) |
92 |
|
sseq1 |
⊢ ( 𝑧 = 𝑢 → ( 𝑧 ⊆ 𝑦 ↔ 𝑢 ⊆ 𝑦 ) ) |
93 |
92
|
rabbidv |
⊢ ( 𝑧 = 𝑢 → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ) |
94 |
93
|
cbvmptv |
⊢ ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) = ( 𝑢 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ) |
95 |
2 94
|
eqtri |
⊢ 𝐹 = ( 𝑢 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ) |
96 |
|
ineq1 |
⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = ( { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) |
97 |
|
inrab |
⊢ ( { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦 ) } |
98 |
|
unss |
⊢ ( ( 𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦 ) ↔ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 ) |
99 |
98
|
rabbii |
⊢ { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦 ) } = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } |
100 |
97 99
|
eqtri |
⊢ ( { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } |
101 |
96 100
|
eqtrdi |
⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) |
102 |
101
|
pweqd |
⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) |
103 |
102
|
ineq2d |
⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) = ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ) |
104 |
103
|
neeq1d |
⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ↔ ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) ) |
105 |
104
|
ralbidv |
⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ↔ ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) ) |
106 |
95 105
|
ralrnmptw |
⊢ ( ∀ 𝑢 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∈ V → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ↔ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) ) |
107 |
91 106
|
syl |
⊢ ( 𝐴 ∈ V → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ↔ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) ) |
108 |
88 107
|
mpbird |
⊢ ( 𝐴 ∈ V → ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ) |
109 |
|
rabexg |
⊢ ( 𝑆 ∈ V → { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ∈ V ) |
110 |
10 109
|
syl |
⊢ ( 𝐴 ∈ V → { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ∈ V ) |
111 |
110
|
ralrimivw |
⊢ ( 𝐴 ∈ V → ∀ 𝑣 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ∈ V ) |
112 |
|
sseq1 |
⊢ ( 𝑧 = 𝑣 → ( 𝑧 ⊆ 𝑦 ↔ 𝑣 ⊆ 𝑦 ) ) |
113 |
112
|
rabbidv |
⊢ ( 𝑧 = 𝑣 → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) |
114 |
113
|
cbvmptv |
⊢ ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) = ( 𝑣 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) |
115 |
2 114
|
eqtri |
⊢ 𝐹 = ( 𝑣 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) |
116 |
|
ineq2 |
⊢ ( 𝑏 = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } → ( 𝑎 ∩ 𝑏 ) = ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) |
117 |
116
|
pweqd |
⊢ ( 𝑏 = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } → 𝒫 ( 𝑎 ∩ 𝑏 ) = 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) |
118 |
117
|
ineq2d |
⊢ ( 𝑏 = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } → ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) = ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ) |
119 |
118
|
neeq1d |
⊢ ( 𝑏 = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } → ( ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ↔ ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ) ) |
120 |
115 119
|
ralrnmptw |
⊢ ( ∀ 𝑣 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ∈ V → ( ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ↔ ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ) ) |
121 |
111 120
|
syl |
⊢ ( 𝐴 ∈ V → ( ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ↔ ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ) ) |
122 |
121
|
ralbidv |
⊢ ( 𝐴 ∈ V → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ↔ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ) ) |
123 |
108 122
|
mpbird |
⊢ ( 𝐴 ∈ V → ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ) |
124 |
33 49 123
|
3jca |
⊢ ( 𝐴 ∈ V → ( ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran 𝐹 ∧ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ) ) |
125 |
|
isfbas |
⊢ ( 𝑆 ∈ V → ( ran 𝐹 ∈ ( fBas ‘ 𝑆 ) ↔ ( ran 𝐹 ⊆ 𝒫 𝑆 ∧ ( ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran 𝐹 ∧ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ) ) ) ) |
126 |
10 125
|
syl |
⊢ ( 𝐴 ∈ V → ( ran 𝐹 ∈ ( fBas ‘ 𝑆 ) ↔ ( ran 𝐹 ⊆ 𝒫 𝑆 ∧ ( ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran 𝐹 ∧ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ) ) ) ) |
127 |
16 124 126
|
mpbir2and |
⊢ ( 𝐴 ∈ V → ran 𝐹 ∈ ( fBas ‘ 𝑆 ) ) |
128 |
3 127
|
eqeltrid |
⊢ ( 𝐴 ∈ V → 𝐿 ∈ ( fBas ‘ 𝑆 ) ) |
129 |
4 5 128
|
3syl |
⊢ ( 𝜑 → 𝐿 ∈ ( fBas ‘ 𝑆 ) ) |