MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnelfm Structured version   Visualization version   GIF version

Theorem rnelfm 22489
Description: A condition for a filter to be an image filter for a given function. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
Assertion
Ref Expression
rnelfm ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ran 𝐹𝐿))

Proof of Theorem rnelfm
Dummy variables 𝑏 𝑠 𝑡 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 filtop 22391 . . . . . . 7 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
213ad2ant2 1126 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑋𝐿)
3 simp1 1128 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑌𝐴)
4 simp3 1130 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝐹:𝑌𝑋)
5 fmf 22481 . . . . . 6 ((𝑋𝐿𝑌𝐴𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
62, 3, 4, 5syl3anc 1363 . . . . 5 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
76ffnd 6508 . . . 4 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌))
8 fvelrnb 6719 . . . 4 ((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿))
97, 8syl 17 . . 3 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿))
10 ffn 6507 . . . . . . . . . . . 12 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
11 dffn4 6589 . . . . . . . . . . . 12 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
1210, 11sylib 219 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
13 foima 6588 . . . . . . . . . . 11 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
1412, 13syl 17 . . . . . . . . . 10 (𝐹:𝑌𝑋 → (𝐹𝑌) = ran 𝐹)
1514ad2antlr 723 . . . . . . . . 9 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹𝑌) = ran 𝐹)
16 simpll 763 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑋𝐿)
17 simpr 485 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑏 ∈ (fBas‘𝑌))
18 simplr 765 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝐹:𝑌𝑋)
19 fgcl 22414 . . . . . . . . . . . 12 (𝑏 ∈ (fBas‘𝑌) → (𝑌filGen𝑏) ∈ (Fil‘𝑌))
20 filtop 22391 . . . . . . . . . . . 12 ((𝑌filGen𝑏) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏))
2119, 20syl 17 . . . . . . . . . . 11 (𝑏 ∈ (fBas‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏))
2221adantl 482 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑌 ∈ (𝑌filGen𝑏))
23 eqid 2818 . . . . . . . . . . 11 (𝑌filGen𝑏) = (𝑌filGen𝑏)
2423imaelfm 22487 . . . . . . . . . 10 (((𝑋𝐿𝑏 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝑏)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏))
2516, 17, 18, 22, 24syl31anc 1365 . . . . . . . . 9 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏))
2615, 25eqeltrrd 2911 . . . . . . . 8 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏))
27 eleq2 2898 . . . . . . . 8 (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → (ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏) ↔ ran 𝐹𝐿))
2826, 27syl5ibcom 246 . . . . . . 7 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿))
2928ex 413 . . . . . 6 ((𝑋𝐿𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
301, 29sylan 580 . . . . 5 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
31303adant1 1122 . . . 4 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
3231rexlimdv 3280 . . 3 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿))
339, 32sylbid 241 . 2 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) → ran 𝐹𝐿))
34 simpl2 1184 . . . . . . . . 9 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 ∈ (Fil‘𝑋))
35 filelss 22388 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡𝐿) → 𝑡𝑋)
3635ex 413 . . . . . . . . 9 (𝐿 ∈ (Fil‘𝑋) → (𝑡𝐿𝑡𝑋))
3734, 36syl 17 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿𝑡𝑋))
38 simpr 485 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → 𝑡𝐿)
39 eqidd 2819 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹𝑡) = (𝐹𝑡))
40 imaeq2 5918 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
4140rspceeqv 3635 . . . . . . . . . . . 12 ((𝑡𝐿 ∧ (𝐹𝑡) = (𝐹𝑡)) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
4238, 39, 41syl2anc 584 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
43 simpl1 1183 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌𝐴)
44 cnvimass 5942 . . . . . . . . . . . . . . . . 17 (𝐹𝑡) ⊆ dom 𝐹
45 fdm 6515 . . . . . . . . . . . . . . . . 17 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
4644, 45sseqtrid 4016 . . . . . . . . . . . . . . . 16 (𝐹:𝑌𝑋 → (𝐹𝑡) ⊆ 𝑌)
47463ad2ant3 1127 . . . . . . . . . . . . . . 15 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹𝑡) ⊆ 𝑌)
4847adantr 481 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑡) ⊆ 𝑌)
4943, 48ssexd 5219 . . . . . . . . . . . . 13 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑡) ∈ V)
50 eqid 2818 . . . . . . . . . . . . . 14 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
5150elrnmpt 5821 . . . . . . . . . . . . 13 ((𝐹𝑡) ∈ V → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5249, 51syl 17 . . . . . . . . . . . 12 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5352adantr 481 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5442, 53mpbird 258 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
55 ssid 3986 . . . . . . . . . . 11 (𝐹𝑡) ⊆ (𝐹𝑡)
56 ffun 6510 . . . . . . . . . . . . . 14 (𝐹:𝑌𝑋 → Fun 𝐹)
57563ad2ant3 1127 . . . . . . . . . . . . 13 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → Fun 𝐹)
5857ad2antrr 722 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → Fun 𝐹)
59 funimass3 6816 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ (𝐹𝑡) ⊆ dom 𝐹) → ((𝐹 “ (𝐹𝑡)) ⊆ 𝑡 ↔ (𝐹𝑡) ⊆ (𝐹𝑡)))
6058, 44, 59sylancl 586 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ((𝐹 “ (𝐹𝑡)) ⊆ 𝑡 ↔ (𝐹𝑡) ⊆ (𝐹𝑡)))
6155, 60mpbiri 259 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
62 imaeq2 5918 . . . . . . . . . . . 12 (𝑠 = (𝐹𝑡) → (𝐹𝑠) = (𝐹 “ (𝐹𝑡)))
6362sseq1d 3995 . . . . . . . . . . 11 (𝑠 = (𝐹𝑡) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡))
6463rspcev 3620 . . . . . . . . . 10 (((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)
6554, 61, 64syl2anc 584 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)
6665ex 413 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡))
6737, 66jcad 513 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 → (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
6834adantr 481 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝐿 ∈ (Fil‘𝑋))
6950elrnmpt 5821 . . . . . . . . . . . . . 14 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
7069elv 3497 . . . . . . . . . . . . 13 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
71 ssid 3986 . . . . . . . . . . . . . . . . . . . 20 (𝐹𝑥) ⊆ (𝐹𝑥)
7257ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → Fun 𝐹)
73 cnvimass 5942 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ⊆ dom 𝐹
74 funimass3 6816 . . . . . . . . . . . . . . . . . . . . 21 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ↔ (𝐹𝑥) ⊆ (𝐹𝑥)))
7572, 73, 74sylancl 586 . . . . . . . . . . . . . . . . . . . 20 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ↔ (𝐹𝑥) ⊆ (𝐹𝑥)))
7671, 75mpbiri 259 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ⊆ 𝑥)
77 imassrn 5933 . . . . . . . . . . . . . . . . . . 19 (𝐹 “ (𝐹𝑥)) ⊆ ran 𝐹
78 ssin 4204 . . . . . . . . . . . . . . . . . . 19 (((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ∧ (𝐹 “ (𝐹𝑥)) ⊆ ran 𝐹) ↔ (𝐹 “ (𝐹𝑥)) ⊆ (𝑥 ∩ ran 𝐹))
7976, 77, 78sylanblc 589 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ⊆ (𝑥 ∩ ran 𝐹))
80 elin 4166 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑧𝑥𝑧 ∈ ran 𝐹))
81 fvelrnb 6719 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 Fn 𝑌 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8210, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝑌𝑋 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
83823ad2ant3 1127 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8483ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8572ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → Fun 𝐹)
8685, 73jctir 521 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → (Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹))
8757ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → Fun 𝐹)
8887ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → Fun 𝐹)
89453ad2ant3 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → dom 𝐹 = 𝑌)
9089ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → dom 𝐹 = 𝑌)
9190eleq2d 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑦 ∈ dom 𝐹𝑦𝑌))
9291biimpar 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → 𝑦 ∈ dom 𝐹)
93 fvimacnv 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
9488, 92, 93syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
9594biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → 𝑦 ∈ (𝐹𝑥))
96 funfvima2 6984 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → (𝑦 ∈ (𝐹𝑥) → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))))
9786, 95, 96sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥)))
9897ex 413 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))))
99 eleq1 2897 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ 𝑥𝑧𝑥))
100 eleq1 2897 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥)) ↔ 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
10199, 100imbi12d 346 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑦) = 𝑧 → (((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))) ↔ (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
10298, 101syl5ibcom 246 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) = 𝑧 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
103102rexlimdva 3281 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (∃𝑦𝑌 (𝐹𝑦) = 𝑧 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
10484, 103sylbid 241 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ ran 𝐹 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
105104impcomd 412 . . . . . . . . . . . . . . . . . . . 20 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝑧𝑥𝑧 ∈ ran 𝐹) → 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
10680, 105syl5bi 243 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ (𝑥 ∩ ran 𝐹) → 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
107106ssrdv 3970 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ (𝐹 “ (𝐹𝑥)))
10879, 107eqssd 3981 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) = (𝑥 ∩ ran 𝐹))
109 filin 22390 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
1101093exp 1111 . . . . . . . . . . . . . . . . . . . . 21 (𝐿 ∈ (Fil‘𝑋) → (𝑥𝐿 → (ran 𝐹𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
111110com23 86 . . . . . . . . . . . . . . . . . . . 20 (𝐿 ∈ (Fil‘𝑋) → (ran 𝐹𝐿 → (𝑥𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
1121113ad2ant2 1126 . . . . . . . . . . . . . . . . . . 19 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (ran 𝐹𝐿 → (𝑥𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
113112imp31 418 . . . . . . . . . . . . . . . . . 18 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
114113adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
115108, 114eqeltrd 2910 . . . . . . . . . . . . . . . 16 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)
116115exp32 421 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)))
117 imaeq2 5918 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐹𝑥) → (𝐹𝑠) = (𝐹 “ (𝐹𝑥)))
118117sseq1d 3995 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡))
119117eleq1d 2894 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ∈ 𝐿 ↔ (𝐹 “ (𝐹𝑥)) ∈ 𝐿))
120119imbi2d 342 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐹𝑥) → ((𝑡𝑋 → (𝐹𝑠) ∈ 𝐿) ↔ (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)))
121118, 120imbi12d 346 . . . . . . . . . . . . . . 15 (𝑠 = (𝐹𝑥) → (((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿)) ↔ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿))))
122116, 121syl5ibrcom 248 . . . . . . . . . . . . . 14 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
123122rexlimdva 3281 . . . . . . . . . . . . 13 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
12470, 123syl5bi 243 . . . . . . . . . . . 12 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
125124imp44 429 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → (𝐹𝑠) ∈ 𝐿)
126 simprr 769 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝑡𝑋)
127 simprlr 776 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → (𝐹𝑠) ⊆ 𝑡)
128 filss 22389 . . . . . . . . . . 11 ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝐹𝑠) ∈ 𝐿𝑡𝑋 ∧ (𝐹𝑠) ⊆ 𝑡)) → 𝑡𝐿)
12968, 125, 126, 127, 128syl13anc 1364 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝑡𝐿)
130129exp44 438 . . . . . . . . 9 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
131130rexlimdv 3280 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
132131impcomd 412 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡) → 𝑡𝐿))
13367, 132impbid 213 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
1342adantr 481 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑋𝐿)
135 rnelfmlem 22488 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
136 simpl3 1185 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐹:𝑌𝑋)
137 elfm 22483 . . . . . . 7 ((𝑋𝐿 ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
138134, 135, 136, 137syl3anc 1363 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
139133, 138bitr4d 283 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥)))))
140139eqrdv 2816 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 = ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))))
1417adantr 481 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌))
142 fnfvelrn 6840 . . . . 5 (((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ ran (𝑋 FilMap 𝐹))
143141, 135, 142syl2anc 584 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ ran (𝑋 FilMap 𝐹))
144140, 143eqeltrd 2910 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 ∈ ran (𝑋 FilMap 𝐹))
145144ex 413 . 2 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (ran 𝐹𝐿𝐿 ∈ ran (𝑋 FilMap 𝐹)))
14633, 145impbid 213 1 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ran 𝐹𝐿))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wrex 3136  Vcvv 3492  cin 3932  wss 3933  cmpt 5137  ccnv 5547  dom cdm 5548  ran crn 5549  cima 5551  Fun wfun 6342   Fn wfn 6343  wf 6344  ontowfo 6346  cfv 6348  (class class class)co 7145  fBascfbas 20461  filGencfg 20462  Filcfil 22381   FilMap cfm 22469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-fbas 20470  df-fg 20471  df-fil 22382  df-fm 22474
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator