Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) |
2 | | filelss 22749 |
. . . . 5
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡 ∈ 𝐿) → 𝑡 ⊆ 𝑋) |
3 | 2 | ex 416 |
. . . 4
⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋)) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋)) |
5 | | fmfnfm.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) |
6 | | mptexg 7037 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
7 | | rnexg 7682 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (Fil‘𝑋) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
10 | | unexg 7534 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
11 | 5, 9, 10 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
12 | | ssfii 9035 |
. . . . . . . . 9
⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
13 | 12 | unssbd 4102 |
. . . . . . . 8
⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
14 | 11, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
15 | 14 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
16 | | eqid 2737 |
. . . . . . . . 9
⊢ (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡) |
17 | | imaeq2 5925 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑡)) |
18 | 17 | rspceeqv 3552 |
. . . . . . . . 9
⊢ ((𝑡 ∈ 𝐿 ∧ (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡)) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) |
19 | 16, 18 | mpan2 691 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝐿 → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) |
20 | 19 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) |
21 | | elfvdm 6749 |
. . . . . . . . . . 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 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ 𝑡) ⊆ 𝑌) |
26 | 22, 25 | ssexd 5217 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ 𝑡) ∈ V) |
27 | 26 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ V) |
28 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) |
29 | 28 | elrnmpt 5825 |
. . . . . . . 8
⊢ ((◡𝐹 “ 𝑡) ∈ V → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))) |
30 | 27, 29 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))) |
31 | 20, 30 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |
32 | 15, 31 | sseldd 3902 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
33 | | ffun 6548 |
. . . . . . . 8
⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹) |
34 | | ssid 3923 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡) |
35 | | funimass2 6463 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡)) → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
36 | 33, 34, 35 | sylancl 589 |
. . . . . . 7
⊢ (𝐹:𝑌⟶𝑋 → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
37 | 24, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
38 | 37 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
39 | | imaeq2 5925 |
. . . . . . 7
⊢ (𝑠 = (◡𝐹 “ 𝑡) → (𝐹 “ 𝑠) = (𝐹 “ (◡𝐹 “ 𝑡))) |
40 | 39 | sseq1d 3932 |
. . . . . 6
⊢ (𝑠 = (◡𝐹 “ 𝑡) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡)) |
41 | 40 | rspcev 3537 |
. . . . 5
⊢ (((◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∧ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) |
42 | 32, 38, 41 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) |
43 | 42 | ex 416 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝐿 → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)) |
44 | 4, 43 | jcad 516 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝐿 → (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |
45 | | elfiun 9046 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)))) |
46 | 5, 9, 45 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)))) |
47 | | fmfnfm.fm |
. . . . . . 7
⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
48 | 5, 1, 24, 47 | fmfnfmlem1 22851 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
49 | 5, 1, 24, 47 | fmfnfmlem3 22853 |
. . . . . . . 8
⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |
50 | 49 | eleq2d 2823 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) |
51 | 28 | elrnmpt 5825 |
. . . . . . . . 9
⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥))) |
52 | 51 | elv 3414 |
. . . . . . . 8
⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥)) |
53 | 5, 1, 24, 47 | fmfnfmlem2 22852 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
54 | 52, 53 | syl5bi 245 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
55 | 50, 54 | sylbid 243 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
56 | 49 | eleq2d 2823 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) |
57 | 28 | elrnmpt 5825 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))) |
58 | 57 | elv 3414 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥)) |
59 | 56, 58 | bitrdi 290 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))) |
60 | 59 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))) |
61 | | fbssfi 22734 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) |
62 | 5, 61 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) |
63 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝐿 ∈ (Fil‘𝑋)) |
64 | 1 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝐿 ∈ (Fil‘𝑋)) |
65 | 47 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
66 | | filtop 22752 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿) |
67 | 1, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑋 ∈ 𝐿) |
68 | 67, 5, 24 | 3jca 1130 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
69 | 68 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
70 | | ssfg 22769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵)) |
71 | 5, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen𝐵)) |
72 | 71 | sselda 3901 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ (𝑌filGen𝐵)) |
73 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵) |
74 | 73 | imaelfm 22848 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
75 | 69, 72, 74 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
76 | 65, 75 | sseldd 3902 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ 𝐿) |
77 | 76 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐹 “ 𝑠) ∈ 𝐿) |
78 | 64, 77 | jca 515 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿)) |
79 | | filin 22751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
80 | 79 | 3expa 1120 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
81 | 78, 80 | sylan 583 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
82 | 81 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
83 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ⊆ 𝑋) |
84 | | elin 3882 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) ↔ (𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥)) |
85 | 24, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → Fun 𝐹) |
86 | | fvelima 6778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Fun
𝐹 ∧ 𝑤 ∈ (𝐹 “ 𝑠)) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤) |
87 | 86 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Fun
𝐹 → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤)) |
88 | 85, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤)) |
89 | 88 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤)) |
90 | 85 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → Fun 𝐹) |
91 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → 𝑠 ⊆ 𝑧) |
92 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → 𝑦 ∈ 𝑠) |
93 | | ssel2 3895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑠 ⊆ 𝑧 ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑧) |
94 | 91, 92, 93 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ 𝑧) |
95 | 85 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → Fun 𝐹) |
96 | | fbelss 22730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
97 | 5, 96 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
98 | 24 | fdmd 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → dom 𝐹 = 𝑌) |
99 | 98 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → dom 𝐹 = 𝑌) |
100 | 97, 99 | sseqtrrd 3942 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ dom 𝐹) |
101 | 100 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝑠 ⊆ dom 𝐹) |
102 | 101 | sselda 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ dom 𝐹) |
103 | | fvimacnv 6873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
104 | 95, 102, 103 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
105 | 104 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → 𝑦 ∈ (◡𝐹 “ 𝑥))) |
106 | 105 | impr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → 𝑦 ∈ (◡𝐹 “ 𝑥)) |
107 | 106 | ad2ant2rl 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (◡𝐹 “ 𝑥)) |
108 | 94, 107 | elind 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥))) |
109 | | inss2 4144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ (◡𝐹 “ 𝑥) |
110 | | cnvimass 5949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹 |
111 | 109, 110 | sstri 3910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ dom 𝐹 |
112 | | funfvima2 7047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Fun
𝐹 ∧ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ dom 𝐹) → (𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
113 | 111, 112 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
𝐹 → (𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
114 | 90, 108, 113 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
115 | 114 | anassrs 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
116 | 115 | expr 460 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
117 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑤 ∈ 𝑥)) |
118 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
119 | 117, 118 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹‘𝑦) = 𝑤 → (((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) ↔ (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
120 | 116, 119 | syl5ibcom 248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
121 | 120 | rexlimdva 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
122 | 89, 121 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ (𝐹 “ 𝑠) → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
123 | 122 | impd 414 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → ((𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
124 | 84, 123 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
125 | 124 | adantrl 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
126 | 125 | ssrdv 3907 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
127 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡) |
128 | 126, 127 | sstrd 3911 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡) |
129 | | filss 22750 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡)) → 𝑡 ∈ 𝐿) |
130 | 63, 82, 83, 128, 129 | syl13anc 1374 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ∈ 𝐿) |
131 | 130 | exp32 424 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
132 | | ineq2 4121 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (◡𝐹 “ 𝑥) → (𝑧 ∩ 𝑤) = (𝑧 ∩ (◡𝐹 “ 𝑥))) |
133 | 132 | imaeq2d 5929 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (◡𝐹 “ 𝑥) → (𝐹 “ (𝑧 ∩ 𝑤)) = (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
134 | 133 | sseq1d 3932 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡)) |
135 | 134 | imbi1d 345 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (◡𝐹 “ 𝑥) → (((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
136 | 131, 135 | syl5ibrcom 250 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → (𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
137 | 136 | rexlimdva 3203 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
138 | 137 | rexlimdvaa 3204 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))) |
139 | 138 | imp 410 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
140 | 62, 139 | syldan 594 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
141 | 60, 140 | sylbid 243 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
142 | 141 | impr 458 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
143 | | imaeq2 5925 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑧 ∩ 𝑤) → (𝐹 “ 𝑠) = (𝐹 “ (𝑧 ∩ 𝑤))) |
144 | 143 | sseq1d 3932 |
. . . . . . . . 9
⊢ (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡)) |
145 | 144 | imbi1d 345 |
. . . . . . . 8
⊢ (𝑠 = (𝑧 ∩ 𝑤) → (((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
146 | 142, 145 | syl5ibrcom 250 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
147 | 146 | rexlimdvva 3213 |
. . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
148 | 48, 55, 147 | 3jaod 1430 |
. . . . 5
⊢ (𝜑 → ((𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
149 | 46, 148 | sylbid 243 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
150 | 149 | rexlimdv 3202 |
. . 3
⊢ (𝜑 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
151 | 150 | impcomd 415 |
. 2
⊢ (𝜑 → ((𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) → 𝑡 ∈ 𝐿)) |
152 | 44, 151 | impbid 215 |
1
⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |