| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | filtop 23864 | . . . . . . 7
⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿) | 
| 2 | 1 | 3ad2ant2 1134 | . . . . . 6
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ 𝐿) | 
| 3 |  | simp1 1136 | . . . . . 6
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 ∈ 𝐴) | 
| 4 |  | simp3 1138 | . . . . . 6
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝐹:𝑌⟶𝑋) | 
| 5 |  | fmf 23954 | . . . . . 6
⊢ ((𝑋 ∈ 𝐿 ∧ 𝑌 ∈ 𝐴 ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋)) | 
| 6 | 2, 3, 4, 5 | syl3anc 1372 | . . . . 5
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋)) | 
| 7 | 6 | ffnd 6736 | . . . 4
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌)) | 
| 8 |  | fvelrnb 6968 | . . . 4
⊢ ((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿)) | 
| 9 | 7, 8 | syl 17 | . . 3
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿)) | 
| 10 |  | ffn 6735 | . . . . . . . . . . . 12
⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌) | 
| 11 |  | dffn4 6825 | . . . . . . . . . . . 12
⊢ (𝐹 Fn 𝑌 ↔ 𝐹:𝑌–onto→ran 𝐹) | 
| 12 | 10, 11 | sylib 218 | . . . . . . . . . . 11
⊢ (𝐹:𝑌⟶𝑋 → 𝐹:𝑌–onto→ran 𝐹) | 
| 13 |  | foima 6824 | . . . . . . . . . . 11
⊢ (𝐹:𝑌–onto→ran 𝐹 → (𝐹 “ 𝑌) = ran 𝐹) | 
| 14 | 12, 13 | syl 17 | . . . . . . . . . 10
⊢ (𝐹:𝑌⟶𝑋 → (𝐹 “ 𝑌) = ran 𝐹) | 
| 15 | 14 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹 “ 𝑌) = ran 𝐹) | 
| 16 |  | simpll 766 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑋 ∈ 𝐿) | 
| 17 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑏 ∈ (fBas‘𝑌)) | 
| 18 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝐹:𝑌⟶𝑋) | 
| 19 |  | fgcl 23887 | . . . . . . . . . . . 12
⊢ (𝑏 ∈ (fBas‘𝑌) → (𝑌filGen𝑏) ∈ (Fil‘𝑌)) | 
| 20 |  | filtop 23864 | . . . . . . . . . . . 12
⊢ ((𝑌filGen𝑏) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏)) | 
| 21 | 19, 20 | syl 17 | . . . . . . . . . . 11
⊢ (𝑏 ∈ (fBas‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏)) | 
| 22 | 21 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑌 ∈ (𝑌filGen𝑏)) | 
| 23 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑌filGen𝑏) = (𝑌filGen𝑏) | 
| 24 | 23 | imaelfm 23960 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝑏 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑌 ∈ (𝑌filGen𝑏)) → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏)) | 
| 25 | 16, 17, 18, 22, 24 | syl31anc 1374 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏)) | 
| 26 | 15, 25 | eqeltrrd 2841 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏)) | 
| 27 |  | eleq2 2829 | . . . . . . . 8
⊢ (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → (ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏) ↔ ran 𝐹 ∈ 𝐿)) | 
| 28 | 26, 27 | syl5ibcom 245 | . . . . . . 7
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹 ∈ 𝐿)) | 
| 29 | 28 | ex 412 | . . . . . 6
⊢ ((𝑋 ∈ 𝐿 ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹 ∈ 𝐿))) | 
| 30 | 1, 29 | sylan 580 | . . . . 5
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹 ∈ 𝐿))) | 
| 31 | 30 | 3adant1 1130 | . . . 4
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹 ∈ 𝐿))) | 
| 32 | 31 | rexlimdv 3152 | . . 3
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹 ∈ 𝐿)) | 
| 33 | 9, 32 | sylbid 240 | . 2
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) → ran 𝐹 ∈ 𝐿)) | 
| 34 |  | simpl2 1192 | . . . . . . . . 9
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝐿 ∈ (Fil‘𝑋)) | 
| 35 |  | filelss 23861 | . . . . . . . . . 10
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡 ∈ 𝐿) → 𝑡 ⊆ 𝑋) | 
| 36 | 35 | ex 412 | . . . . . . . . 9
⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋)) | 
| 37 | 34, 36 | syl 17 | . . . . . . . 8
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋)) | 
| 38 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑡 ∈ 𝐿) → 𝑡 ∈ 𝐿) | 
| 39 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡)) | 
| 40 |  | imaeq2 6073 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑡 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑡)) | 
| 41 | 40 | rspceeqv 3644 | . . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝐿 ∧ (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡)) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) | 
| 42 | 38, 39, 41 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑡 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)) | 
| 43 |  | simpl1 1191 | . . . . . . . . . . . . . 14
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ 𝐴) | 
| 44 |  | cnvimass 6099 | . . . . . . . . . . . . . . . . 17
⊢ (◡𝐹 “ 𝑡) ⊆ dom 𝐹 | 
| 45 |  | fdm 6744 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌) | 
| 46 | 44, 45 | sseqtrid 4025 | . . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑌⟶𝑋 → (◡𝐹 “ 𝑡) ⊆ 𝑌) | 
| 47 | 46 | 3ad2ant3 1135 | . . . . . . . . . . . . . . 15
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (◡𝐹 “ 𝑡) ⊆ 𝑌) | 
| 48 | 47 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (◡𝐹 “ 𝑡) ⊆ 𝑌) | 
| 49 | 43, 48 | ssexd 5323 | . . . . . . . . . . . . 13
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ V) | 
| 50 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) | 
| 51 | 50 | elrnmpt 5968 | . . . . . . . . . . . . 13
⊢ ((◡𝐹 “ 𝑡) ∈ V → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))) | 
| 52 | 49, 51 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑡 ∈ 𝐿) → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))) | 
| 54 | 42, 53 | mpbird 257 | . . . . . . . . . 10
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) | 
| 55 |  | ssid 4005 | . . . . . . . . . . 11
⊢ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡) | 
| 56 |  | ffun 6738 | . . . . . . . . . . . . . 14
⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹) | 
| 57 | 56 | 3ad2ant3 1135 | . . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → Fun 𝐹) | 
| 58 | 57 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑡 ∈ 𝐿) → Fun 𝐹) | 
| 59 |  | funimass3 7073 | . . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝑡) ⊆ dom 𝐹) → ((𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡 ↔ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡))) | 
| 60 | 58, 44, 59 | sylancl 586 | . . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑡 ∈ 𝐿) → ((𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡 ↔ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡))) | 
| 61 | 55, 60 | mpbiri 258 | . . . . . . . . . 10
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑡 ∈ 𝐿) → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) | 
| 62 |  | imaeq2 6073 | . . . . . . . . . . . 12
⊢ (𝑠 = (◡𝐹 “ 𝑡) → (𝐹 “ 𝑠) = (𝐹 “ (◡𝐹 “ 𝑡))) | 
| 63 | 62 | sseq1d 4014 | . . . . . . . . . . 11
⊢ (𝑠 = (◡𝐹 “ 𝑡) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡)) | 
| 64 | 63 | rspcev 3621 | . . . . . . . . . 10
⊢ (((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝐹 “ 𝑠) ⊆ 𝑡) | 
| 65 | 54, 61, 64 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑡 ∈ 𝐿) → ∃𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝐹 “ 𝑠) ⊆ 𝑡) | 
| 66 | 65 | ex 412 | . . . . . . . 8
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑡 ∈ 𝐿 → ∃𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝐹 “ 𝑠) ⊆ 𝑡)) | 
| 67 | 37, 66 | jcad 512 | . . . . . . 7
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑡 ∈ 𝐿 → (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝐹 “ 𝑠) ⊆ 𝑡))) | 
| 68 | 34 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ (𝐹 “ 𝑠) ⊆ 𝑡) ∧ 𝑡 ⊆ 𝑋)) → 𝐿 ∈ (Fil‘𝑋)) | 
| 69 | 50 | elrnmpt 5968 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥))) | 
| 70 | 69 | elv 3484 | . . . . . . . . . . . . 13
⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥)) | 
| 71 |  | ssid 4005 | . . . . . . . . . . . . . . . . . . . 20
⊢ (◡𝐹 “ 𝑥) ⊆ (◡𝐹 “ 𝑥) | 
| 72 | 57 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → Fun 𝐹) | 
| 73 |  | cnvimass 6099 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹 | 
| 74 |  | funimass3 7073 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝑥) ⊆ dom 𝐹) → ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑥 ↔ (◡𝐹 “ 𝑥) ⊆ (◡𝐹 “ 𝑥))) | 
| 75 | 72, 73, 74 | sylancl 586 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑥 ↔ (◡𝐹 “ 𝑥) ⊆ (◡𝐹 “ 𝑥))) | 
| 76 | 71, 75 | mpbiri 258 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑥) | 
| 77 |  | imassrn 6088 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ ran 𝐹 | 
| 78 |  | ssin 4238 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑥 ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ ran 𝐹) ↔ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ (𝑥 ∩ ran 𝐹)) | 
| 79 | 76, 77, 78 | sylanblc 589 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ (𝑥 ∩ ran 𝐹)) | 
| 80 |  | elin 3966 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ∈ ran 𝐹)) | 
| 81 |  | fvelrnb 6968 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹 Fn 𝑌 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑌 (𝐹‘𝑦) = 𝑧)) | 
| 82 | 10, 81 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:𝑌⟶𝑋 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑌 (𝐹‘𝑦) = 𝑧)) | 
| 83 | 82 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑌 (𝐹‘𝑦) = 𝑧)) | 
| 84 | 83 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑌 (𝐹‘𝑦) = 𝑧)) | 
| 85 | 72 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝑌 ∈
𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) ∧ 𝑦 ∈ 𝑌) ∧ (𝐹‘𝑦) ∈ 𝑥) → Fun 𝐹) | 
| 86 | 85, 73 | jctir 520 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑌 ∈
𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) ∧ 𝑦 ∈ 𝑌) ∧ (𝐹‘𝑦) ∈ 𝑥) → (Fun 𝐹 ∧ (◡𝐹 “ 𝑥) ⊆ dom 𝐹)) | 
| 87 | 57 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → Fun 𝐹) | 
| 88 | 87 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) ∧ 𝑦 ∈ 𝑌) → Fun 𝐹) | 
| 89 | 45 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → dom 𝐹 = 𝑌) | 
| 90 | 89 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → dom 𝐹 = 𝑌) | 
| 91 | 90 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝑌)) | 
| 92 | 91 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ dom 𝐹) | 
| 93 |  | fvimacnv 7072 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) | 
| 94 | 88, 92, 93 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) ∧ 𝑦 ∈ 𝑌) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) | 
| 95 | 94 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑌 ∈
𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) ∧ 𝑦 ∈ 𝑌) ∧ (𝐹‘𝑦) ∈ 𝑥) → 𝑦 ∈ (◡𝐹 “ 𝑥)) | 
| 96 |  | funfvima2 7252 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝑥) ⊆ dom 𝐹) → (𝑦 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑦) ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) | 
| 97 | 86, 95, 96 | sylc 65 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝑌 ∈
𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) ∧ 𝑦 ∈ 𝑌) ∧ (𝐹‘𝑦) ∈ 𝑥) → (𝐹‘𝑦) ∈ (𝐹 “ (◡𝐹 “ 𝑥))) | 
| 98 | 97 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) ∧ 𝑦 ∈ 𝑌) → ((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) | 
| 99 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹‘𝑦) = 𝑧 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) | 
| 100 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹‘𝑦) = 𝑧 → ((𝐹‘𝑦) ∈ (𝐹 “ (◡𝐹 “ 𝑥)) ↔ 𝑧 ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) | 
| 101 | 99, 100 | imbi12d 344 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘𝑦) = 𝑧 → (((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (◡𝐹 “ 𝑥))) ↔ (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝐹 “ (◡𝐹 “ 𝑥))))) | 
| 102 | 98, 101 | syl5ibcom 245 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) ∧ 𝑦 ∈ 𝑌) → ((𝐹‘𝑦) = 𝑧 → (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝐹 “ (◡𝐹 “ 𝑥))))) | 
| 103 | 102 | rexlimdva 3154 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (∃𝑦 ∈ 𝑌 (𝐹‘𝑦) = 𝑧 → (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝐹 “ (◡𝐹 “ 𝑥))))) | 
| 104 | 84, 103 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑧 ∈ ran 𝐹 → (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝐹 “ (◡𝐹 “ 𝑥))))) | 
| 105 | 104 | impcomd 411 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ∈ ran 𝐹) → 𝑧 ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) | 
| 106 | 80, 105 | biimtrid 242 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑧 ∈ (𝑥 ∩ ran 𝐹) → 𝑧 ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) | 
| 107 | 106 | ssrdv 3988 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ (𝐹 “ (◡𝐹 “ 𝑥))) | 
| 108 | 79, 107 | eqssd 4000 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ (◡𝐹 “ 𝑥)) = (𝑥 ∩ ran 𝐹)) | 
| 109 |  | filin 23863 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿) | 
| 110 | 109 | 3exp 1119 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐿 → (ran 𝐹 ∈ 𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿))) | 
| 111 | 110 | com23 86 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ∈ (Fil‘𝑋) → (ran 𝐹 ∈ 𝐿 → (𝑥 ∈ 𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿))) | 
| 112 | 111 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (ran 𝐹 ∈ 𝐿 → (𝑥 ∈ 𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿))) | 
| 113 | 112 | imp31 417 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿) | 
| 114 | 113 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿) | 
| 115 | 108, 114 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ (◡𝐹 “ 𝑥)) ∈ 𝐿) | 
| 116 | 115 | exp32 420 | . . . . . . . . . . . . . . 15
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → (𝐹 “ (◡𝐹 “ 𝑥)) ∈ 𝐿))) | 
| 117 |  | imaeq2 6073 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (◡𝐹 “ 𝑥) → (𝐹 “ 𝑠) = (𝐹 “ (◡𝐹 “ 𝑥))) | 
| 118 | 117 | sseq1d 4014 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡)) | 
| 119 | 117 | eleq1d 2825 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ∈ 𝐿 ↔ (𝐹 “ (◡𝐹 “ 𝑥)) ∈ 𝐿)) | 
| 120 | 119 | imbi2d 340 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = (◡𝐹 “ 𝑥) → ((𝑡 ⊆ 𝑋 → (𝐹 “ 𝑠) ∈ 𝐿) ↔ (𝑡 ⊆ 𝑋 → (𝐹 “ (◡𝐹 “ 𝑥)) ∈ 𝐿))) | 
| 121 | 118, 120 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ (𝑠 = (◡𝐹 “ 𝑥) → (((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → (𝐹 “ 𝑠) ∈ 𝐿)) ↔ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → (𝐹 “ (◡𝐹 “ 𝑥)) ∈ 𝐿)))) | 
| 122 | 116, 121 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → (𝐹 “ 𝑠) ∈ 𝐿)))) | 
| 123 | 122 | rexlimdva 3154 | . . . . . . . . . . . . 13
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → (𝐹 “ 𝑠) ∈ 𝐿)))) | 
| 124 | 70, 123 | biimtrid 242 | . . . . . . . . . . . 12
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → (𝐹 “ 𝑠) ∈ 𝐿)))) | 
| 125 | 124 | imp44 428 | . . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ (𝐹 “ 𝑠) ⊆ 𝑡) ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ 𝑠) ∈ 𝐿) | 
| 126 |  | simprr 772 | . . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ (𝐹 “ 𝑠) ⊆ 𝑡) ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ⊆ 𝑋) | 
| 127 |  | simprlr 779 | . . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ (𝐹 “ 𝑠) ⊆ 𝑡) ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ 𝑠) ⊆ 𝑡) | 
| 128 |  | filss 23862 | . . . . . . . . . . 11
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ (𝐹 “ 𝑠) ⊆ 𝑡)) → 𝑡 ∈ 𝐿) | 
| 129 | 68, 125, 126, 127, 128 | syl13anc 1373 | . . . . . . . . . 10
⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ (𝐹 “ 𝑠) ⊆ 𝑡) ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ∈ 𝐿) | 
| 130 | 129 | exp44 437 | . . . . . . . . 9
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) | 
| 131 | 130 | rexlimdv 3152 | . . . . . . . 8
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) | 
| 132 | 131 | impcomd 411 | . . . . . . 7
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝐹 “ 𝑠) ⊆ 𝑡) → 𝑡 ∈ 𝐿)) | 
| 133 | 67, 132 | impbid 212 | . . . . . 6
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝐹 “ 𝑠) ⊆ 𝑡))) | 
| 134 | 2 | adantr 480 | . . . . . . 7
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑋 ∈ 𝐿) | 
| 135 |  | rnelfmlem 23961 | . . . . . . 7
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) | 
| 136 |  | simpl3 1193 | . . . . . . 7
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝐹:𝑌⟶𝑋) | 
| 137 |  | elfm 23956 | . . . . . . 7
⊢ ((𝑋 ∈ 𝐿 ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝐹 “ 𝑠) ⊆ 𝑡))) | 
| 138 | 134, 135,
136, 137 | syl3anc 1372 | . . . . . 6
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝐹 “ 𝑠) ⊆ 𝑡))) | 
| 139 | 133, 138 | bitr4d 282 | . . . . 5
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑡 ∈ 𝐿 ↔ 𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) | 
| 140 | 139 | eqrdv 2734 | . . . 4
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝐿 = ((𝑋 FilMap 𝐹)‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) | 
| 141 | 7 | adantr 480 | . . . . 5
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌)) | 
| 142 |  | fnfvelrn 7099 | . . . . 5
⊢ (((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) → ((𝑋 FilMap 𝐹)‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ ran (𝑋 FilMap 𝐹)) | 
| 143 | 141, 135,
142 | syl2anc 584 | . . . 4
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑋 FilMap 𝐹)‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ ran (𝑋 FilMap 𝐹)) | 
| 144 | 140, 143 | eqeltrd 2840 | . . 3
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝐿 ∈ ran (𝑋 FilMap 𝐹)) | 
| 145 | 144 | ex 412 | . 2
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (ran 𝐹 ∈ 𝐿 → 𝐿 ∈ ran (𝑋 FilMap 𝐹))) | 
| 146 | 33, 145 | impbid 212 | 1
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ran 𝐹 ∈ 𝐿)) |