Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) |
2 | | filelss 22460 |
. . . . 5
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡 ∈ 𝐿) → 𝑡 ⊆ 𝑋) |
3 | 2 | ex 415 |
. . . 4
⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋)) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋)) |
5 | | fmfnfm.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) |
6 | | mptexg 6984 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
7 | | rnexg 7614 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (Fil‘𝑋) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
10 | | unexg 7472 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
11 | 5, 9, 10 | syl2anc 586 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
12 | | ssfii 8883 |
. . . . . . . . 9
⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
13 | 12 | unssbd 4164 |
. . . . . . . 8
⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
14 | 11, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
15 | 14 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
16 | | eqid 2821 |
. . . . . . . . 9
⊢ (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡) |
17 | | imaeq2 5925 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑡)) |
18 | 17 | rspceeqv 3638 |
. . . . . . . . 9
⊢ ((𝑡 ∈ 𝐿 ∧ (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡)) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) |
19 | 16, 18 | mpan2 689 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝐿 → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) |
20 | 19 | adantl 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) |
21 | | elfvdm 6702 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas) |
22 | 5, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ dom fBas) |
23 | | cnvimass 5949 |
. . . . . . . . . . 11
⊢ (◡𝐹 “ 𝑡) ⊆ dom 𝐹 |
24 | | fmfnfm.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝑌⟶𝑋) |
25 | 23, 24 | fssdm 6530 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ 𝑡) ⊆ 𝑌) |
26 | 22, 25 | ssexd 5228 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ 𝑡) ∈ V) |
27 | 26 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ V) |
28 | | eqid 2821 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) |
29 | 28 | elrnmpt 5828 |
. . . . . . . 8
⊢ ((◡𝐹 “ 𝑡) ∈ V → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))) |
30 | 27, 29 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))) |
31 | 20, 30 | mpbird 259 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |
32 | 15, 31 | sseldd 3968 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
33 | | ffun 6517 |
. . . . . . . 8
⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹) |
34 | | ssid 3989 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡) |
35 | | funimass2 6437 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡)) → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
36 | 33, 34, 35 | sylancl 588 |
. . . . . . 7
⊢ (𝐹:𝑌⟶𝑋 → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
37 | 24, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
38 | 37 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
39 | | imaeq2 5925 |
. . . . . . 7
⊢ (𝑠 = (◡𝐹 “ 𝑡) → (𝐹 “ 𝑠) = (𝐹 “ (◡𝐹 “ 𝑡))) |
40 | 39 | sseq1d 3998 |
. . . . . 6
⊢ (𝑠 = (◡𝐹 “ 𝑡) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡)) |
41 | 40 | rspcev 3623 |
. . . . 5
⊢ (((◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∧ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) |
42 | 32, 38, 41 | syl2anc 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) |
43 | 42 | ex 415 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝐿 → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)) |
44 | 4, 43 | jcad 515 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝐿 → (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |
45 | | elfiun 8894 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)))) |
46 | 5, 9, 45 | syl2anc 586 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)))) |
47 | | fmfnfm.fm |
. . . . . . 7
⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
48 | 5, 1, 24, 47 | fmfnfmlem1 22562 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
49 | 5, 1, 24, 47 | fmfnfmlem3 22564 |
. . . . . . . 8
⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |
50 | 49 | eleq2d 2898 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) |
51 | 28 | elrnmpt 5828 |
. . . . . . . . 9
⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥))) |
52 | 51 | elv 3499 |
. . . . . . . 8
⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥)) |
53 | 5, 1, 24, 47 | fmfnfmlem2 22563 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
54 | 52, 53 | syl5bi 244 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
55 | 50, 54 | sylbid 242 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
56 | 49 | eleq2d 2898 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) |
57 | 28 | elrnmpt 5828 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))) |
58 | 57 | elv 3499 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥)) |
59 | 56, 58 | syl6bb 289 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))) |
60 | 59 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))) |
61 | | fbssfi 22445 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) |
62 | 5, 61 | sylan 582 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) |
63 | 1 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝐿 ∈ (Fil‘𝑋)) |
64 | 1 | adantr 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝐿 ∈ (Fil‘𝑋)) |
65 | 47 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
66 | | filtop 22463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿) |
67 | 1, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑋 ∈ 𝐿) |
68 | 67, 5, 24 | 3jca 1124 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
69 | 68 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
70 | | ssfg 22480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵)) |
71 | 5, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen𝐵)) |
72 | 71 | sselda 3967 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ (𝑌filGen𝐵)) |
73 | | eqid 2821 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵) |
74 | 73 | imaelfm 22559 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
75 | 69, 72, 74 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
76 | 65, 75 | sseldd 3968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ 𝐿) |
77 | 76 | adantrr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐹 “ 𝑠) ∈ 𝐿) |
78 | 64, 77 | jca 514 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿)) |
79 | | filin 22462 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
80 | 79 | 3expa 1114 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
81 | 78, 80 | sylan 582 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
82 | 81 | adantr 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
83 | | simprr 771 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ⊆ 𝑋) |
84 | | elin 4169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) ↔ (𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥)) |
85 | 24, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → Fun 𝐹) |
86 | | fvelima 6731 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Fun
𝐹 ∧ 𝑤 ∈ (𝐹 “ 𝑠)) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤) |
87 | 86 | ex 415 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Fun
𝐹 → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤)) |
88 | 85, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤)) |
89 | 88 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤)) |
90 | 85 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → Fun 𝐹) |
91 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → 𝑠 ⊆ 𝑧) |
92 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → 𝑦 ∈ 𝑠) |
93 | | ssel2 3962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑠 ⊆ 𝑧 ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑧) |
94 | 91, 92, 93 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ 𝑧) |
95 | 85 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → Fun 𝐹) |
96 | | fbelss 22441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
97 | 5, 96 | sylan 582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
98 | 24 | fdmd 6523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → dom 𝐹 = 𝑌) |
99 | 98 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → dom 𝐹 = 𝑌) |
100 | 97, 99 | sseqtrrd 4008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ dom 𝐹) |
101 | 100 | adantrr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝑠 ⊆ dom 𝐹) |
102 | 101 | sselda 3967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ dom 𝐹) |
103 | | fvimacnv 6823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
104 | 95, 102, 103 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
105 | 104 | biimpd 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → 𝑦 ∈ (◡𝐹 “ 𝑥))) |
106 | 105 | impr 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → 𝑦 ∈ (◡𝐹 “ 𝑥)) |
107 | 106 | ad2ant2rl 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (◡𝐹 “ 𝑥)) |
108 | 94, 107 | elind 4171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥))) |
109 | | inss2 4206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ (◡𝐹 “ 𝑥) |
110 | | cnvimass 5949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹 |
111 | 109, 110 | sstri 3976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ dom 𝐹 |
112 | | funfvima2 6993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Fun
𝐹 ∧ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ dom 𝐹) → (𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
113 | 111, 112 | mpan2 689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
𝐹 → (𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
114 | 90, 108, 113 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
115 | 114 | anassrs 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
116 | 115 | expr 459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
117 | | eleq1 2900 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑤 ∈ 𝑥)) |
118 | | eleq1 2900 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
119 | 117, 118 | imbi12d 347 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹‘𝑦) = 𝑤 → (((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) ↔ (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
120 | 116, 119 | syl5ibcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
121 | 120 | rexlimdva 3284 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
122 | 89, 121 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ (𝐹 “ 𝑠) → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
123 | 122 | impd 413 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → ((𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
124 | 84, 123 | syl5bi 244 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
125 | 124 | adantrl 714 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
126 | 125 | ssrdv 3973 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
127 | | simprl 769 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡) |
128 | 126, 127 | sstrd 3977 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡) |
129 | | filss 22461 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡)) → 𝑡 ∈ 𝐿) |
130 | 63, 82, 83, 128, 129 | syl13anc 1368 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ∈ 𝐿) |
131 | 130 | exp32 423 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
132 | | ineq2 4183 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (◡𝐹 “ 𝑥) → (𝑧 ∩ 𝑤) = (𝑧 ∩ (◡𝐹 “ 𝑥))) |
133 | 132 | imaeq2d 5929 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (◡𝐹 “ 𝑥) → (𝐹 “ (𝑧 ∩ 𝑤)) = (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
134 | 133 | sseq1d 3998 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡)) |
135 | 134 | imbi1d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (◡𝐹 “ 𝑥) → (((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
136 | 131, 135 | syl5ibrcom 249 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → (𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
137 | 136 | rexlimdva 3284 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
138 | 137 | rexlimdvaa 3285 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))) |
139 | 138 | imp 409 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
140 | 62, 139 | syldan 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
141 | 60, 140 | sylbid 242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
142 | 141 | impr 457 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
143 | | imaeq2 5925 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑧 ∩ 𝑤) → (𝐹 “ 𝑠) = (𝐹 “ (𝑧 ∩ 𝑤))) |
144 | 143 | sseq1d 3998 |
. . . . . . . . 9
⊢ (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡)) |
145 | 144 | imbi1d 344 |
. . . . . . . 8
⊢ (𝑠 = (𝑧 ∩ 𝑤) → (((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
146 | 142, 145 | syl5ibrcom 249 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
147 | 146 | rexlimdvva 3294 |
. . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
148 | 48, 55, 147 | 3jaod 1424 |
. . . . 5
⊢ (𝜑 → ((𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
149 | 46, 148 | sylbid 242 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
150 | 149 | rexlimdv 3283 |
. . 3
⊢ (𝜑 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
151 | 150 | impcomd 414 |
. 2
⊢ (𝜑 → ((𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) → 𝑡 ∈ 𝐿)) |
152 | 44, 151 | impbid 214 |
1
⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |