| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fmfnfm.l | . . . . . 6
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) | 
| 2 | 1 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝐿 ∈ (Fil‘𝑋)) | 
| 3 |  | simplr 768 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑥 ∈ 𝐿) | 
| 4 |  | fmfnfm.fm | . . . . . . . 8
⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) | 
| 5 |  | fmfnfm.f | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑌⟶𝑋) | 
| 6 |  | ffn 6735 | . . . . . . . . . . 11
⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌) | 
| 7 |  | dffn4 6825 | . . . . . . . . . . 11
⊢ (𝐹 Fn 𝑌 ↔ 𝐹:𝑌–onto→ran 𝐹) | 
| 8 | 6, 7 | sylib 218 | . . . . . . . . . 10
⊢ (𝐹:𝑌⟶𝑋 → 𝐹:𝑌–onto→ran 𝐹) | 
| 9 |  | foima 6824 | . . . . . . . . . 10
⊢ (𝐹:𝑌–onto→ran 𝐹 → (𝐹 “ 𝑌) = ran 𝐹) | 
| 10 | 5, 8, 9 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) = ran 𝐹) | 
| 11 |  | filtop 23864 | . . . . . . . . . . 11
⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿) | 
| 12 | 1, 11 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐿) | 
| 13 |  | fmfnfm.b | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) | 
| 14 |  | fgcl 23887 | . . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌)) | 
| 15 |  | filtop 23864 | . . . . . . . . . . 11
⊢ ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵)) | 
| 16 | 13, 14, 15 | 3syl 18 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐵)) | 
| 17 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵) | 
| 18 | 17 | imaelfm 23960 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) | 
| 19 | 12, 13, 5, 16, 18 | syl31anc 1374 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) | 
| 20 | 10, 19 | eqeltrrd 2841 | . . . . . . . 8
⊢ (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵)) | 
| 21 | 4, 20 | sseldd 3983 | . . . . . . 7
⊢ (𝜑 → ran 𝐹 ∈ 𝐿) | 
| 22 | 21 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ran 𝐹 ∈ 𝐿) | 
| 23 |  | filin 23863 | . . . . . 6
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿) | 
| 24 | 2, 3, 22, 23 | syl3anc 1372 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿) | 
| 25 |  | simprr 772 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ⊆ 𝑋) | 
| 26 |  | elin 3966 | . . . . . . 7
⊢ (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹)) | 
| 27 |  | fvelrnb 6968 | . . . . . . . . . . . 12
⊢ (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦)) | 
| 28 | 5, 6, 27 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦)) | 
| 29 | 28 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦)) | 
| 30 | 5 | ffund 6739 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → Fun 𝐹) | 
| 31 | 30 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → Fun 𝐹) | 
| 32 |  | simprr 772 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → 𝑧 ∈ 𝑌) | 
| 33 | 5 | fdmd 6745 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝑌) | 
| 34 | 33 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → dom 𝐹 = 𝑌) | 
| 35 | 32, 34 | eleqtrrd 2843 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → 𝑧 ∈ dom 𝐹) | 
| 36 |  | fvimacnv 7072 | . . . . . . . . . . . . . . 15
⊢ ((Fun
𝐹 ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (◡𝐹 “ 𝑥))) | 
| 37 | 31, 35, 36 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (◡𝐹 “ 𝑥))) | 
| 38 |  | cnvimass 6099 | . . . . . . . . . . . . . . . 16
⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹 | 
| 39 |  | funfvima2 7252 | . . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝑥) ⊆ dom 𝐹) → (𝑧 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) | 
| 40 | 31, 38, 39 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → (𝑧 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) | 
| 41 |  | ssel 3976 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → ((𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)) → (𝐹‘𝑧) ∈ 𝑡)) | 
| 42 | 41 | ad2antrl 728 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)) → (𝐹‘𝑧) ∈ 𝑡)) | 
| 43 | 40, 42 | syld 47 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → (𝑧 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑧) ∈ 𝑡)) | 
| 44 | 37, 43 | sylbid 240 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) ∈ 𝑥 → (𝐹‘𝑧) ∈ 𝑡)) | 
| 45 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) | 
| 46 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑡 ↔ 𝑦 ∈ 𝑡)) | 
| 47 | 45, 46 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) = 𝑦 → (((𝐹‘𝑧) ∈ 𝑥 → (𝐹‘𝑧) ∈ 𝑡) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) | 
| 48 | 44, 47 | syl5ibcom 245 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) = 𝑦 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) | 
| 49 | 48 | expr 456 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑧 ∈ 𝑌 → ((𝐹‘𝑧) = 𝑦 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡)))) | 
| 50 | 49 | rexlimdv 3152 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) | 
| 51 | 29, 50 | sylbid 240 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) | 
| 52 | 51 | impcomd 411 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ 𝑡)) | 
| 53 | 52 | adantrr 717 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ 𝑡)) | 
| 54 | 26, 53 | biimtrid 242 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑦 ∈ (𝑥 ∩ ran 𝐹) → 𝑦 ∈ 𝑡)) | 
| 55 | 54 | ssrdv 3988 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ 𝑡) | 
| 56 |  | filss 23862 | . . . . 5
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝑥 ∩ ran 𝐹) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ (𝑥 ∩ ran 𝐹) ⊆ 𝑡)) → 𝑡 ∈ 𝐿) | 
| 57 | 2, 24, 25, 55, 56 | syl13anc 1373 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ∈ 𝐿) | 
| 58 | 57 | exp32 420 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) | 
| 59 |  | imaeq2 6073 | . . . . 5
⊢ (𝑠 = (◡𝐹 “ 𝑥) → (𝐹 “ 𝑠) = (𝐹 “ (◡𝐹 “ 𝑥))) | 
| 60 | 59 | sseq1d 4014 | . . . 4
⊢ (𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡)) | 
| 61 | 60 | imbi1d 341 | . . 3
⊢ (𝑠 = (◡𝐹 “ 𝑥) → (((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) | 
| 62 | 58, 61 | syl5ibrcom 247 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐿) → (𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) | 
| 63 | 62 | rexlimdva 3154 | 1
⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |