| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fmfnfm.b |
⊢ ( 𝜑 → 𝐵 ∈ ( fBas ‘ 𝑌 ) ) |
| 2 |
|
fmfnfm.l |
⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑋 ) ) |
| 3 |
|
fmfnfm.f |
⊢ ( 𝜑 → 𝐹 : 𝑌 ⟶ 𝑋 ) |
| 4 |
|
fmfnfm.fm |
⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 ) |
| 5 |
|
filelss |
⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ∈ 𝐿 ) → 𝑡 ⊆ 𝑋 ) |
| 6 |
5
|
ex |
⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ( 𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋 ) ) |
| 7 |
2 6
|
syl |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋 ) ) |
| 8 |
|
mptexg |
⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V ) |
| 9 |
|
rnexg |
⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V ) |
| 10 |
8 9
|
syl |
⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V ) |
| 11 |
2 10
|
syl |
⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V ) |
| 12 |
|
unexg |
⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V ) → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V ) |
| 13 |
1 11 12
|
syl2anc |
⊢ ( 𝜑 → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V ) |
| 14 |
|
ssfii |
⊢ ( ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V → ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 15 |
14
|
unssbd |
⊢ ( ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∈ V → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 16 |
13 15
|
syl |
⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 17 |
16
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 18 |
|
eqid |
⊢ ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑡 ) |
| 19 |
|
imaeq2 |
⊢ ( 𝑥 = 𝑡 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑡 ) ) |
| 20 |
19
|
rspceeqv |
⊢ ( ( 𝑡 ∈ 𝐿 ∧ ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑡 ) ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) |
| 21 |
18 20
|
mpan2 |
⊢ ( 𝑡 ∈ 𝐿 → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) |
| 22 |
21
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) |
| 23 |
|
elfvdm |
⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝑌 ∈ dom fBas ) |
| 24 |
1 23
|
syl |
⊢ ( 𝜑 → 𝑌 ∈ dom fBas ) |
| 25 |
|
cnvimass |
⊢ ( ◡ 𝐹 “ 𝑡 ) ⊆ dom 𝐹 |
| 26 |
25 3
|
fssdm |
⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑡 ) ⊆ 𝑌 ) |
| 27 |
24 26
|
ssexd |
⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑡 ) ∈ V ) |
| 28 |
27
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) ∈ V ) |
| 29 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) |
| 30 |
29
|
elrnmpt |
⊢ ( ( ◡ 𝐹 “ 𝑡 ) ∈ V → ( ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 31 |
28 30
|
syl |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( ◡ 𝐹 “ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 32 |
22 31
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 33 |
17 32
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( ◡ 𝐹 “ 𝑡 ) ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 34 |
|
ffun |
⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → Fun 𝐹 ) |
| 35 |
|
ssid |
⊢ ( ◡ 𝐹 “ 𝑡 ) ⊆ ( ◡ 𝐹 “ 𝑡 ) |
| 36 |
|
funimass2 |
⊢ ( ( Fun 𝐹 ∧ ( ◡ 𝐹 “ 𝑡 ) ⊆ ( ◡ 𝐹 “ 𝑡 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) |
| 37 |
34 35 36
|
sylancl |
⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) |
| 38 |
3 37
|
syl |
⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) |
| 39 |
38
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) |
| 40 |
|
imaeq2 |
⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑡 ) → ( 𝐹 “ 𝑠 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ) |
| 41 |
40
|
sseq1d |
⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑡 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) ) |
| 42 |
41
|
rspcev |
⊢ ( ( ( ◡ 𝐹 “ 𝑡 ) ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑡 ) ) ⊆ 𝑡 ) → ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) |
| 43 |
33 39 42
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) |
| 44 |
43
|
ex |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 → ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) |
| 45 |
7 44
|
jcad |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) ) |
| 46 |
|
elfiun |
⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V ) → ( 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ↔ ( 𝑠 ∈ ( fi ‘ 𝐵 ) ∨ 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∨ ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ∃ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) 𝑠 = ( 𝑧 ∩ 𝑤 ) ) ) ) |
| 47 |
1 11 46
|
syl2anc |
⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ↔ ( 𝑠 ∈ ( fi ‘ 𝐵 ) ∨ 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∨ ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ∃ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) 𝑠 = ( 𝑧 ∩ 𝑤 ) ) ) ) |
| 48 |
1 2 3 4
|
fmfnfmlem1 |
⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ 𝐵 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 49 |
1 2 3 4
|
fmfnfmlem3 |
⊢ ( 𝜑 → ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 50 |
49
|
eleq2d |
⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 51 |
29
|
elrnmpt |
⊢ ( 𝑠 ∈ V → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 52 |
51
|
elv |
⊢ ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ) |
| 53 |
1 2 3 4
|
fmfnfmlem2 |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 54 |
52 53
|
biimtrid |
⊢ ( 𝜑 → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 55 |
50 54
|
sylbid |
⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 56 |
49
|
eleq2d |
⊢ ( 𝜑 → ( 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ 𝑤 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 57 |
29
|
elrnmpt |
⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 58 |
57
|
elv |
⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) ) |
| 59 |
56 58
|
bitrdi |
⊢ ( 𝜑 → ( 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 60 |
59
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ( 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 61 |
|
fbssfi |
⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 ) |
| 62 |
1 61
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 ) |
| 63 |
2
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) ) |
| 64 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) ) |
| 65 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 ) |
| 66 |
|
filtop |
⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐿 ) |
| 67 |
2 66
|
syl |
⊢ ( 𝜑 → 𝑋 ∈ 𝐿 ) |
| 68 |
67 1 3
|
3jca |
⊢ ( 𝜑 → ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ) |
| 69 |
68
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ) |
| 70 |
|
ssfg |
⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐵 ⊆ ( 𝑌 filGen 𝐵 ) ) |
| 71 |
1 70
|
syl |
⊢ ( 𝜑 → 𝐵 ⊆ ( 𝑌 filGen 𝐵 ) ) |
| 72 |
71
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ∈ ( 𝑌 filGen 𝐵 ) ) |
| 73 |
|
eqid |
⊢ ( 𝑌 filGen 𝐵 ) = ( 𝑌 filGen 𝐵 ) |
| 74 |
73
|
imaelfm |
⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑠 ∈ ( 𝑌 filGen 𝐵 ) ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ) |
| 75 |
69 72 74
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ) |
| 76 |
65 75
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) |
| 77 |
76
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) |
| 78 |
64 77
|
jca |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) ) |
| 79 |
|
filin |
⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 “ 𝑠 ) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 ) |
| 80 |
79
|
3expa |
⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 “ 𝑠 ) ∈ 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 ) |
| 81 |
78 80
|
sylan |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 ) |
| 82 |
81
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 ) |
| 83 |
|
simprr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝑡 ⊆ 𝑋 ) |
| 84 |
|
elin |
⊢ ( 𝑤 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ↔ ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) ∧ 𝑤 ∈ 𝑥 ) ) |
| 85 |
3 34
|
syl |
⊢ ( 𝜑 → Fun 𝐹 ) |
| 86 |
|
fvelima |
⊢ ( ( Fun 𝐹 ∧ 𝑤 ∈ ( 𝐹 “ 𝑠 ) ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 ) |
| 87 |
86
|
ex |
⊢ ( Fun 𝐹 → ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 ) ) |
| 88 |
85 87
|
syl |
⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 ) ) |
| 89 |
88
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) → ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 ) ) |
| 90 |
85
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → Fun 𝐹 ) |
| 91 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) → 𝑠 ⊆ 𝑧 ) |
| 92 |
|
simprl |
⊢ ( ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) → 𝑦 ∈ 𝑠 ) |
| 93 |
|
ssel2 |
⊢ ( ( 𝑠 ⊆ 𝑧 ∧ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ 𝑧 ) |
| 94 |
91 92 93
|
syl2an |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → 𝑦 ∈ 𝑧 ) |
| 95 |
85
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑦 ∈ 𝑠 ) → Fun 𝐹 ) |
| 96 |
|
fbelss |
⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ⊆ 𝑌 ) |
| 97 |
1 96
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ⊆ 𝑌 ) |
| 98 |
3
|
fdmd |
⊢ ( 𝜑 → dom 𝐹 = 𝑌 ) |
| 99 |
98
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → dom 𝐹 = 𝑌 ) |
| 100 |
97 99
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ⊆ dom 𝐹 ) |
| 101 |
100
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → 𝑠 ⊆ dom 𝐹 ) |
| 102 |
101
|
sselda |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ dom 𝐹 ) |
| 103 |
|
fvimacnv |
⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 104 |
95 102 103
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 105 |
104
|
biimpd |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 106 |
105
|
impr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) → 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) |
| 107 |
106
|
ad2ant2rl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) |
| 108 |
94 107
|
elind |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → 𝑦 ∈ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 109 |
|
inss2 |
⊢ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( ◡ 𝐹 “ 𝑥 ) |
| 110 |
|
cnvimass |
⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹 |
| 111 |
109 110
|
sstri |
⊢ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ dom 𝐹 |
| 112 |
|
funfvima2 |
⊢ ( ( Fun 𝐹 ∧ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ dom 𝐹 ) → ( 𝑦 ∈ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 113 |
111 112
|
mpan2 |
⊢ ( Fun 𝐹 → ( 𝑦 ∈ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 114 |
90 108 113
|
sylc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝑡 ⊆ 𝑋 ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 115 |
114
|
anassrs |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ ( 𝑦 ∈ 𝑠 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 116 |
115
|
expr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 117 |
|
eleq1 |
⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ↔ 𝑤 ∈ 𝑥 ) ) |
| 118 |
|
eleq1 |
⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 119 |
117 118
|
imbi12d |
⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ↔ ( 𝑤 ∈ 𝑥 → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) |
| 120 |
116 119
|
syl5ibcom |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) |
| 121 |
120
|
rexlimdva |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑠 ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) |
| 122 |
89 121
|
syld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) ) |
| 123 |
122
|
impd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( ( 𝑤 ∈ ( 𝐹 “ 𝑠 ) ∧ 𝑤 ∈ 𝑥 ) → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 124 |
84 123
|
biimtrid |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ 𝑡 ⊆ 𝑋 ) → ( 𝑤 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 125 |
124
|
adantrl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑤 ∈ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) → 𝑤 ∈ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) |
| 126 |
125
|
ssrdv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ⊆ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 127 |
|
simprl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ) |
| 128 |
126 127
|
sstrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ⊆ 𝑡 ) |
| 129 |
|
filss |
⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ ( ( 𝐹 “ 𝑠 ) ∩ 𝑥 ) ⊆ 𝑡 ) ) → 𝑡 ∈ 𝐿 ) |
| 130 |
63 82 83 128 129
|
syl13anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝑡 ∈ 𝐿 ) |
| 131 |
130
|
exp32 |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) |
| 132 |
|
ineq2 |
⊢ ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( 𝑧 ∩ 𝑤 ) = ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 133 |
132
|
imaeq2d |
⊢ ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) = ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 134 |
133
|
sseq1d |
⊢ ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 ↔ ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 ) ) |
| 135 |
134
|
imbi1d |
⊢ ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ↔ ( ( 𝐹 “ ( 𝑧 ∩ ( ◡ 𝐹 “ 𝑥 ) ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 136 |
131 135
|
syl5ibrcom |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 137 |
136
|
rexlimdva |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧 ) ) → ( ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 138 |
137
|
rexlimdvaa |
⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 → ( ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) ) |
| 139 |
138
|
imp |
⊢ ( ( 𝜑 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 ) → ( ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 140 |
62 139
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐿 𝑤 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 141 |
60 140
|
sylbid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( fi ‘ 𝐵 ) ) → ( 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 142 |
141
|
impr |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) → ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) |
| 143 |
|
imaeq2 |
⊢ ( 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( 𝐹 “ 𝑠 ) = ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ) |
| 144 |
143
|
sseq1d |
⊢ ( 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ↔ ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 ) ) |
| 145 |
144
|
imbi1d |
⊢ ( 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ↔ ( ( 𝐹 “ ( 𝑧 ∩ 𝑤 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 146 |
142 145
|
syl5ibrcom |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ) → ( 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 147 |
146
|
rexlimdvva |
⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ∃ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) 𝑠 = ( 𝑧 ∩ 𝑤 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 148 |
48 55 147
|
3jaod |
⊢ ( 𝜑 → ( ( 𝑠 ∈ ( fi ‘ 𝐵 ) ∨ 𝑠 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ∨ ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ∃ 𝑤 ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) 𝑠 = ( 𝑧 ∩ 𝑤 ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 149 |
47 148
|
sylbid |
⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) ) |
| 150 |
149
|
rexlimdv |
⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) |
| 151 |
150
|
impcomd |
⊢ ( 𝜑 → ( ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) → 𝑡 ∈ 𝐿 ) ) |
| 152 |
45 151
|
impbid |
⊢ ( 𝜑 → ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ ( fi ‘ ( 𝐵 ∪ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ) ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ) ) ) |