| Step | Hyp | Ref
| Expression |
| 1 | | fmfnfm.l |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) |
| 2 | | filelss 23860 |
. . . . 5
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡 ∈ 𝐿) → 𝑡 ⊆ 𝑋) |
| 3 | 2 | ex 412 |
. . . 4
⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋)) |
| 4 | 1, 3 | syl 17 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋)) |
| 5 | | fmfnfm.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) |
| 6 | | mptexg 7241 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
| 7 | | rnexg 7924 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (Fil‘𝑋) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
| 9 | 1, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
| 10 | | unexg 7763 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
| 11 | 5, 9, 10 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
| 12 | | ssfii 9459 |
. . . . . . . . 9
⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 13 | 12 | unssbd 4194 |
. . . . . . . 8
⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 14 | 11, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 15 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 16 | | eqid 2737 |
. . . . . . . . 9
⊢ (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡) |
| 17 | | imaeq2 6074 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑡)) |
| 18 | 17 | rspceeqv 3645 |
. . . . . . . . 9
⊢ ((𝑡 ∈ 𝐿 ∧ (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡)) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) |
| 19 | 16, 18 | mpan2 691 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝐿 → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) |
| 20 | 19 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) |
| 21 | | elfvdm 6943 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas) |
| 22 | 5, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ dom fBas) |
| 23 | | cnvimass 6100 |
. . . . . . . . . . 11
⊢ (◡𝐹 “ 𝑡) ⊆ dom 𝐹 |
| 24 | | fmfnfm.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝑌⟶𝑋) |
| 25 | 23, 24 | fssdm 6755 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ 𝑡) ⊆ 𝑌) |
| 26 | 22, 25 | ssexd 5324 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ 𝑡) ∈ V) |
| 27 | 26 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ V) |
| 28 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) |
| 29 | 28 | elrnmpt 5969 |
. . . . . . . 8
⊢ ((◡𝐹 “ 𝑡) ∈ V → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))) |
| 30 | 27, 29 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))) |
| 31 | 20, 30 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |
| 32 | 15, 31 | sseldd 3984 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 33 | | ffun 6739 |
. . . . . . . 8
⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹) |
| 34 | | ssid 4006 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡) |
| 35 | | funimass2 6649 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡)) → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
| 36 | 33, 34, 35 | sylancl 586 |
. . . . . . 7
⊢ (𝐹:𝑌⟶𝑋 → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
| 37 | 24, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
| 38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) |
| 39 | | imaeq2 6074 |
. . . . . . 7
⊢ (𝑠 = (◡𝐹 “ 𝑡) → (𝐹 “ 𝑠) = (𝐹 “ (◡𝐹 “ 𝑡))) |
| 40 | 39 | sseq1d 4015 |
. . . . . 6
⊢ (𝑠 = (◡𝐹 “ 𝑡) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡)) |
| 41 | 40 | rspcev 3622 |
. . . . 5
⊢ (((◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∧ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) |
| 42 | 32, 38, 41 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) |
| 43 | 42 | ex 412 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝐿 → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)) |
| 44 | 4, 43 | jcad 512 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝐿 → (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |
| 45 | | elfiun 9470 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)))) |
| 46 | 5, 9, 45 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)))) |
| 47 | | fmfnfm.fm |
. . . . . . 7
⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
| 48 | 5, 1, 24, 47 | fmfnfmlem1 23962 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 49 | 5, 1, 24, 47 | fmfnfmlem3 23964 |
. . . . . . . 8
⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |
| 50 | 49 | eleq2d 2827 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) |
| 51 | 28 | elrnmpt 5969 |
. . . . . . . . 9
⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥))) |
| 52 | 51 | elv 3485 |
. . . . . . . 8
⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥)) |
| 53 | 5, 1, 24, 47 | fmfnfmlem2 23963 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 54 | 52, 53 | biimtrid 242 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 55 | 50, 54 | sylbid 240 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 56 | 49 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) |
| 57 | 28 | elrnmpt 5969 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))) |
| 58 | 57 | elv 3485 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥)) |
| 59 | 56, 58 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))) |
| 60 | 59 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))) |
| 61 | | fbssfi 23845 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) |
| 62 | 5, 61 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) |
| 63 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝐿 ∈ (Fil‘𝑋)) |
| 64 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝐿 ∈ (Fil‘𝑋)) |
| 65 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
| 66 | | filtop 23863 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿) |
| 67 | 1, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑋 ∈ 𝐿) |
| 68 | 67, 5, 24 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
| 70 | | ssfg 23880 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵)) |
| 71 | 5, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen𝐵)) |
| 72 | 71 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ (𝑌filGen𝐵)) |
| 73 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵) |
| 74 | 73 | imaelfm 23959 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
| 75 | 69, 72, 74 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
| 76 | 65, 75 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ 𝐿) |
| 77 | 76 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐹 “ 𝑠) ∈ 𝐿) |
| 78 | 64, 77 | jca 511 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿)) |
| 79 | | filin 23862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
| 80 | 79 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
| 81 | 78, 80 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
| 83 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ⊆ 𝑋) |
| 84 | | elin 3967 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) ↔ (𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥)) |
| 85 | 24, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → Fun 𝐹) |
| 86 | | fvelima 6974 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Fun
𝐹 ∧ 𝑤 ∈ (𝐹 “ 𝑠)) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤) |
| 87 | 86 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 3978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑠 ⊆ 𝑧 ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑧) |
| 94 | 91, 92, 93 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ 𝑧) |
| 95 | 85 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → Fun 𝐹) |
| 96 | | fbelss 23841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
| 97 | 5, 96 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
| 98 | 24 | fdmd 6746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → dom 𝐹 = 𝑌) |
| 99 | 98 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → dom 𝐹 = 𝑌) |
| 100 | 97, 99 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ dom 𝐹) |
| 101 | 100 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝑠 ⊆ dom 𝐹) |
| 102 | 101 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ dom 𝐹) |
| 103 | | fvimacnv 7073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
| 104 | 95, 102, 103 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
| 105 | 104 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → 𝑦 ∈ (◡𝐹 “ 𝑥))) |
| 106 | 105 | impr 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → 𝑦 ∈ (◡𝐹 “ 𝑥)) |
| 107 | 106 | ad2ant2rl 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (◡𝐹 “ 𝑥)) |
| 108 | 94, 107 | elind 4200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥))) |
| 109 | | inss2 4238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ (◡𝐹 “ 𝑥) |
| 110 | | cnvimass 6100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹 |
| 111 | 109, 110 | sstri 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ dom 𝐹 |
| 112 | | funfvima2 7251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Fun
𝐹 ∧ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ dom 𝐹) → (𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
| 113 | 111, 112 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
𝐹 → (𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
| 114 | 90, 108, 113 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
| 115 | 114 | anassrs 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
| 116 | 115 | expr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
| 117 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑤 ∈ 𝑥)) |
| 118 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
| 119 | 117, 118 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹‘𝑦) = 𝑤 → (((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) ↔ (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
| 120 | 116, 119 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
| 121 | 120 | rexlimdva 3155 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
| 122 | 89, 121 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ (𝐹 “ 𝑠) → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))) |
| 123 | 122 | impd 410 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → ((𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
| 124 | 84, 123 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
| 125 | 124 | adantrl 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))) |
| 126 | 125 | ssrdv 3989 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
| 127 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡) |
| 128 | 126, 127 | sstrd 3994 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡) |
| 129 | | filss 23861 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡)) → 𝑡 ∈ 𝐿) |
| 130 | 63, 82, 83, 128, 129 | syl13anc 1374 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ∈ 𝐿) |
| 131 | 130 | exp32 420 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
| 132 | | ineq2 4214 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (◡𝐹 “ 𝑥) → (𝑧 ∩ 𝑤) = (𝑧 ∩ (◡𝐹 “ 𝑥))) |
| 133 | 132 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (◡𝐹 “ 𝑥) → (𝐹 “ (𝑧 ∩ 𝑤)) = (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) |
| 134 | 133 | sseq1d 4015 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡)) |
| 135 | 134 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (◡𝐹 “ 𝑥) → (((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 136 | 131, 135 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → (𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 137 | 136 | rexlimdva 3155 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 138 | 137 | rexlimdvaa 3156 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))) |
| 139 | 138 | imp 406 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 140 | 62, 139 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 141 | 60, 140 | sylbid 240 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 142 | 141 | impr 454 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
| 143 | | imaeq2 6074 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑧 ∩ 𝑤) → (𝐹 “ 𝑠) = (𝐹 “ (𝑧 ∩ 𝑤))) |
| 144 | 143 | sseq1d 4015 |
. . . . . . . . 9
⊢ (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡)) |
| 145 | 144 | imbi1d 341 |
. . . . . . . 8
⊢ (𝑠 = (𝑧 ∩ 𝑤) → (((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 146 | 142, 145 | syl5ibrcom 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 147 | 146 | rexlimdvva 3213 |
. . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 148 | 48, 55, 147 | 3jaod 1431 |
. . . . 5
⊢ (𝜑 → ((𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 149 | 46, 148 | sylbid 240 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
| 150 | 149 | rexlimdv 3153 |
. . 3
⊢ (𝜑 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
| 151 | 150 | impcomd 411 |
. 2
⊢ (𝜑 → ((𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) → 𝑡 ∈ 𝐿)) |
| 152 | 44, 151 | impbid 212 |
1
⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |