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

Theorem rnelfm 22564
 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 22466 . . . . . . 7 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
213ad2ant2 1131 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑋𝐿)
3 simp1 1133 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑌𝐴)
4 simp3 1135 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝐹:𝑌𝑋)
5 fmf 22556 . . . . . 6 ((𝑋𝐿𝑌𝐴𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
62, 3, 4, 5syl3anc 1368 . . . . 5 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
76ffnd 6504 . . . 4 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌))
8 fvelrnb 6717 . . . 4 ((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿))
97, 8syl 17 . . 3 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿))
10 ffn 6503 . . . . . . . . . . . 12 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
11 dffn4 6587 . . . . . . . . . . . 12 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
1210, 11sylib 221 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
13 foima 6586 . . . . . . . . . . 11 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
1412, 13syl 17 . . . . . . . . . 10 (𝐹:𝑌𝑋 → (𝐹𝑌) = ran 𝐹)
1514ad2antlr 726 . . . . . . . . 9 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹𝑌) = ran 𝐹)
16 simpll 766 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑋𝐿)
17 simpr 488 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑏 ∈ (fBas‘𝑌))
18 simplr 768 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝐹:𝑌𝑋)
19 fgcl 22489 . . . . . . . . . . . 12 (𝑏 ∈ (fBas‘𝑌) → (𝑌filGen𝑏) ∈ (Fil‘𝑌))
20 filtop 22466 . . . . . . . . . . . 12 ((𝑌filGen𝑏) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏))
2119, 20syl 17 . . . . . . . . . . 11 (𝑏 ∈ (fBas‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏))
2221adantl 485 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑌 ∈ (𝑌filGen𝑏))
23 eqid 2824 . . . . . . . . . . 11 (𝑌filGen𝑏) = (𝑌filGen𝑏)
2423imaelfm 22562 . . . . . . . . . 10 (((𝑋𝐿𝑏 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝑏)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏))
2516, 17, 18, 22, 24syl31anc 1370 . . . . . . . . 9 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏))
2615, 25eqeltrrd 2917 . . . . . . . 8 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏))
27 eleq2 2904 . . . . . . . 8 (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → (ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏) ↔ ran 𝐹𝐿))
2826, 27syl5ibcom 248 . . . . . . 7 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿))
2928ex 416 . . . . . 6 ((𝑋𝐿𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
301, 29sylan 583 . . . . 5 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
31303adant1 1127 . . . 4 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
3231rexlimdv 3275 . . 3 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿))
339, 32sylbid 243 . 2 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) → ran 𝐹𝐿))
34 simpl2 1189 . . . . . . . . 9 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 ∈ (Fil‘𝑋))
35 filelss 22463 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡𝐿) → 𝑡𝑋)
3635ex 416 . . . . . . . . 9 (𝐿 ∈ (Fil‘𝑋) → (𝑡𝐿𝑡𝑋))
3734, 36syl 17 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿𝑡𝑋))
38 simpr 488 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → 𝑡𝐿)
39 eqidd 2825 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹𝑡) = (𝐹𝑡))
40 imaeq2 5912 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
4140rspceeqv 3624 . . . . . . . . . . . 12 ((𝑡𝐿 ∧ (𝐹𝑡) = (𝐹𝑡)) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
4238, 39, 41syl2anc 587 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
43 simpl1 1188 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌𝐴)
44 cnvimass 5936 . . . . . . . . . . . . . . . . 17 (𝐹𝑡) ⊆ dom 𝐹
45 fdm 6511 . . . . . . . . . . . . . . . . 17 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
4644, 45sseqtrid 4005 . . . . . . . . . . . . . . . 16 (𝐹:𝑌𝑋 → (𝐹𝑡) ⊆ 𝑌)
47463ad2ant3 1132 . . . . . . . . . . . . . . 15 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹𝑡) ⊆ 𝑌)
4847adantr 484 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑡) ⊆ 𝑌)
4943, 48ssexd 5214 . . . . . . . . . . . . 13 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑡) ∈ V)
50 eqid 2824 . . . . . . . . . . . . . 14 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
5150elrnmpt 5815 . . . . . . . . . . . . 13 ((𝐹𝑡) ∈ V → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5249, 51syl 17 . . . . . . . . . . . 12 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5352adantr 484 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5442, 53mpbird 260 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
55 ssid 3975 . . . . . . . . . . 11 (𝐹𝑡) ⊆ (𝐹𝑡)
56 ffun 6506 . . . . . . . . . . . . . 14 (𝐹:𝑌𝑋 → Fun 𝐹)
57563ad2ant3 1132 . . . . . . . . . . . . 13 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → Fun 𝐹)
5857ad2antrr 725 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → Fun 𝐹)
59 funimass3 6815 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ (𝐹𝑡) ⊆ dom 𝐹) → ((𝐹 “ (𝐹𝑡)) ⊆ 𝑡 ↔ (𝐹𝑡) ⊆ (𝐹𝑡)))
6058, 44, 59sylancl 589 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ((𝐹 “ (𝐹𝑡)) ⊆ 𝑡 ↔ (𝐹𝑡) ⊆ (𝐹𝑡)))
6155, 60mpbiri 261 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
62 imaeq2 5912 . . . . . . . . . . . 12 (𝑠 = (𝐹𝑡) → (𝐹𝑠) = (𝐹 “ (𝐹𝑡)))
6362sseq1d 3984 . . . . . . . . . . 11 (𝑠 = (𝐹𝑡) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡))
6463rspcev 3609 . . . . . . . . . 10 (((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)
6554, 61, 64syl2anc 587 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)
6665ex 416 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡))
6737, 66jcad 516 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 → (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
6834adantr 484 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝐿 ∈ (Fil‘𝑋))
6950elrnmpt 5815 . . . . . . . . . . . . . 14 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
7069elv 3485 . . . . . . . . . . . . 13 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
71 ssid 3975 . . . . . . . . . . . . . . . . . . . 20 (𝐹𝑥) ⊆ (𝐹𝑥)
7257ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → Fun 𝐹)
73 cnvimass 5936 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ⊆ dom 𝐹
74 funimass3 6815 . . . . . . . . . . . . . . . . . . . . 21 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ↔ (𝐹𝑥) ⊆ (𝐹𝑥)))
7572, 73, 74sylancl 589 . . . . . . . . . . . . . . . . . . . 20 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ↔ (𝐹𝑥) ⊆ (𝐹𝑥)))
7671, 75mpbiri 261 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ⊆ 𝑥)
77 imassrn 5927 . . . . . . . . . . . . . . . . . . 19 (𝐹 “ (𝐹𝑥)) ⊆ ran 𝐹
78 ssin 4192 . . . . . . . . . . . . . . . . . . 19 (((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ∧ (𝐹 “ (𝐹𝑥)) ⊆ ran 𝐹) ↔ (𝐹 “ (𝐹𝑥)) ⊆ (𝑥 ∩ ran 𝐹))
7976, 77, 78sylanblc 592 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ⊆ (𝑥 ∩ ran 𝐹))
80 elin 3935 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑧𝑥𝑧 ∈ ran 𝐹))
81 fvelrnb 6717 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 Fn 𝑌 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8210, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝑌𝑋 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
83823ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8483ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8572ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → Fun 𝐹)
8685, 73jctir 524 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → (Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹))
8757ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → Fun 𝐹)
8887ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → Fun 𝐹)
89453ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → dom 𝐹 = 𝑌)
9089ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → dom 𝐹 = 𝑌)
9190eleq2d 2901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑦 ∈ dom 𝐹𝑦𝑌))
9291biimpar 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → 𝑦 ∈ dom 𝐹)
93 fvimacnv 6814 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
9488, 92, 93syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
9594biimpa 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → 𝑦 ∈ (𝐹𝑥))
96 funfvima2 6985 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → (𝑦 ∈ (𝐹𝑥) → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))))
9786, 95, 96sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥)))
9897ex 416 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))))
99 eleq1 2903 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ 𝑥𝑧𝑥))
100 eleq1 2903 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥)) ↔ 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
10199, 100imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑦) = 𝑧 → (((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))) ↔ (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
10298, 101syl5ibcom 248 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) = 𝑧 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
103102rexlimdva 3276 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (∃𝑦𝑌 (𝐹𝑦) = 𝑧 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
10484, 103sylbid 243 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ ran 𝐹 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
105104impcomd 415 . . . . . . . . . . . . . . . . . . . 20 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝑧𝑥𝑧 ∈ ran 𝐹) → 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
10680, 105syl5bi 245 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ (𝑥 ∩ ran 𝐹) → 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
107106ssrdv 3959 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ (𝐹 “ (𝐹𝑥)))
10879, 107eqssd 3970 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) = (𝑥 ∩ ran 𝐹))
109 filin 22465 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
1101093exp 1116 . . . . . . . . . . . . . . . . . . . . 21 (𝐿 ∈ (Fil‘𝑋) → (𝑥𝐿 → (ran 𝐹𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
111110com23 86 . . . . . . . . . . . . . . . . . . . 20 (𝐿 ∈ (Fil‘𝑋) → (ran 𝐹𝐿 → (𝑥𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
1121113ad2ant2 1131 . . . . . . . . . . . . . . . . . . 19 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (ran 𝐹𝐿 → (𝑥𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
113112imp31 421 . . . . . . . . . . . . . . . . . 18 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
114113adantr 484 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
115108, 114eqeltrd 2916 . . . . . . . . . . . . . . . 16 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)
116115exp32 424 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)))
117 imaeq2 5912 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐹𝑥) → (𝐹𝑠) = (𝐹 “ (𝐹𝑥)))
118117sseq1d 3984 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡))
119117eleq1d 2900 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ∈ 𝐿 ↔ (𝐹 “ (𝐹𝑥)) ∈ 𝐿))
120119imbi2d 344 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐹𝑥) → ((𝑡𝑋 → (𝐹𝑠) ∈ 𝐿) ↔ (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)))
121118, 120imbi12d 348 . . . . . . . . . . . . . . 15 (𝑠 = (𝐹𝑥) → (((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿)) ↔ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿))))
122116, 121syl5ibrcom 250 . . . . . . . . . . . . . 14 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
123122rexlimdva 3276 . . . . . . . . . . . . 13 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
12470, 123syl5bi 245 . . . . . . . . . . . 12 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
125124imp44 432 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → (𝐹𝑠) ∈ 𝐿)
126 simprr 772 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝑡𝑋)
127 simprlr 779 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → (𝐹𝑠) ⊆ 𝑡)
128 filss 22464 . . . . . . . . . . 11 ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝐹𝑠) ∈ 𝐿𝑡𝑋 ∧ (𝐹𝑠) ⊆ 𝑡)) → 𝑡𝐿)
12968, 125, 126, 127, 128syl13anc 1369 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝑡𝐿)
130129exp44 441 . . . . . . . . 9 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
131130rexlimdv 3275 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
132131impcomd 415 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡) → 𝑡𝐿))
13367, 132impbid 215 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
1342adantr 484 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑋𝐿)
135 rnelfmlem 22563 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
136 simpl3 1190 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐹:𝑌𝑋)
137 elfm 22558 . . . . . . 7 ((𝑋𝐿 ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
138134, 135, 136, 137syl3anc 1368 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
139133, 138bitr4d 285 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥)))))
140139eqrdv 2822 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 = ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))))
1417adantr 484 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌))
142 fnfvelrn 6839 . . . . 5 (((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ ran (𝑋 FilMap 𝐹))
143141, 135, 142syl2anc 587 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ ran (𝑋 FilMap 𝐹))
144140, 143eqeltrd 2916 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 ∈ ran (𝑋 FilMap 𝐹))
145144ex 416 . 2 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (ran 𝐹𝐿𝐿 ∈ ran (𝑋 FilMap 𝐹)))
14633, 145impbid 215 1 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ran 𝐹𝐿))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115  ∃wrex 3134  Vcvv 3480   ∩ cin 3918   ⊆ wss 3919   ↦ cmpt 5132  ◡ccnv 5541  dom cdm 5542  ran crn 5543   “ cima 5545  Fun wfun 6337   Fn wfn 6338  ⟶wf 6339  –onto→wfo 6341  ‘cfv 6343  (class class class)co 7149  fBascfbas 20086  filGencfg 20087  Filcfil 22456   FilMap cfm 22544 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-fbas 20095  df-fg 20096  df-fil 22457  df-fm 22549 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator