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

Theorem rnelfm 21950
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 21852 . . . . . . 7 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
213ad2ant2 1128 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑋𝐿)
3 simp1 1130 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑌𝐴)
4 simp3 1132 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝐹:𝑌𝑋)
5 fmf 21942 . . . . . 6 ((𝑋𝐿𝑌𝐴𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
62, 3, 4, 5syl3anc 1473 . . . . 5 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
7 ffn 6198 . . . . 5 ((𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌))
86, 7syl 17 . . . 4 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌))
9 fvelrnb 6397 . . . 4 ((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿))
108, 9syl 17 . . 3 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿))
11 ffn 6198 . . . . . . . . . . . 12 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
12 dffn4 6274 . . . . . . . . . . . 12 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
1311, 12sylib 208 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
14 foima 6273 . . . . . . . . . . 11 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
1513, 14syl 17 . . . . . . . . . 10 (𝐹:𝑌𝑋 → (𝐹𝑌) = ran 𝐹)
1615ad2antlr 765 . . . . . . . . 9 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹𝑌) = ran 𝐹)
17 simpll 807 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑋𝐿)
18 simpr 479 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑏 ∈ (fBas‘𝑌))
19 simplr 809 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝐹:𝑌𝑋)
20 fgcl 21875 . . . . . . . . . . . 12 (𝑏 ∈ (fBas‘𝑌) → (𝑌filGen𝑏) ∈ (Fil‘𝑌))
21 filtop 21852 . . . . . . . . . . . 12 ((𝑌filGen𝑏) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏))
2220, 21syl 17 . . . . . . . . . . 11 (𝑏 ∈ (fBas‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏))
2322adantl 473 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑌 ∈ (𝑌filGen𝑏))
24 eqid 2752 . . . . . . . . . . 11 (𝑌filGen𝑏) = (𝑌filGen𝑏)
2524imaelfm 21948 . . . . . . . . . 10 (((𝑋𝐿𝑏 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝑏)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏))
2617, 18, 19, 23, 25syl31anc 1476 . . . . . . . . 9 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏))
2716, 26eqeltrrd 2832 . . . . . . . 8 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏))
28 eleq2 2820 . . . . . . . 8 (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → (ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏) ↔ ran 𝐹𝐿))
2927, 28syl5ibcom 235 . . . . . . 7 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿))
3029ex 449 . . . . . 6 ((𝑋𝐿𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
311, 30sylan 489 . . . . 5 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
32313adant1 1124 . . . 4 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
3332rexlimdv 3160 . . 3 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿))
3410, 33sylbid 230 . 2 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) → ran 𝐹𝐿))
35 simpl2 1227 . . . . . . . . 9 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 ∈ (Fil‘𝑋))
36 filelss 21849 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡𝐿) → 𝑡𝑋)
3736ex 449 . . . . . . . . 9 (𝐿 ∈ (Fil‘𝑋) → (𝑡𝐿𝑡𝑋))
3835, 37syl 17 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿𝑡𝑋))
39 simpr 479 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → 𝑡𝐿)
40 eqidd 2753 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹𝑡) = (𝐹𝑡))
41 imaeq2 5612 . . . . . . . . . . . . . 14 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
4241eqeq2d 2762 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → ((𝐹𝑡) = (𝐹𝑥) ↔ (𝐹𝑡) = (𝐹𝑡)))
4342rspcev 3441 . . . . . . . . . . . 12 ((𝑡𝐿 ∧ (𝐹𝑡) = (𝐹𝑡)) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
4439, 40, 43syl2anc 696 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
45 simpl1 1225 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌𝐴)
46 cnvimass 5635 . . . . . . . . . . . . . . . . 17 (𝐹𝑡) ⊆ dom 𝐹
47 fdm 6204 . . . . . . . . . . . . . . . . 17 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
4846, 47syl5sseq 3786 . . . . . . . . . . . . . . . 16 (𝐹:𝑌𝑋 → (𝐹𝑡) ⊆ 𝑌)
49483ad2ant3 1129 . . . . . . . . . . . . . . 15 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹𝑡) ⊆ 𝑌)
5049adantr 472 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑡) ⊆ 𝑌)
5145, 50ssexd 4949 . . . . . . . . . . . . 13 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑡) ∈ V)
52 eqid 2752 . . . . . . . . . . . . . 14 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
5352elrnmpt 5519 . . . . . . . . . . . . 13 ((𝐹𝑡) ∈ V → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5451, 53syl 17 . . . . . . . . . . . 12 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5554adantr 472 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5644, 55mpbird 247 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
57 ssid 3757 . . . . . . . . . . 11 (𝐹𝑡) ⊆ (𝐹𝑡)
58 ffun 6201 . . . . . . . . . . . . . 14 (𝐹:𝑌𝑋 → Fun 𝐹)
59583ad2ant3 1129 . . . . . . . . . . . . 13 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → Fun 𝐹)
6059ad2antrr 764 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → Fun 𝐹)
61 funimass3 6488 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ (𝐹𝑡) ⊆ dom 𝐹) → ((𝐹 “ (𝐹𝑡)) ⊆ 𝑡 ↔ (𝐹𝑡) ⊆ (𝐹𝑡)))
6260, 46, 61sylancl 697 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ((𝐹 “ (𝐹𝑡)) ⊆ 𝑡 ↔ (𝐹𝑡) ⊆ (𝐹𝑡)))
6357, 62mpbiri 248 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
64 imaeq2 5612 . . . . . . . . . . . 12 (𝑠 = (𝐹𝑡) → (𝐹𝑠) = (𝐹 “ (𝐹𝑡)))
6564sseq1d 3765 . . . . . . . . . . 11 (𝑠 = (𝐹𝑡) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡))
6665rspcev 3441 . . . . . . . . . 10 (((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)
6756, 63, 66syl2anc 696 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)
6867ex 449 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡))
6938, 68jcad 556 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 → (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
7035adantr 472 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝐿 ∈ (Fil‘𝑋))
71 vex 3335 . . . . . . . . . . . . . . 15 𝑠 ∈ V
7252elrnmpt 5519 . . . . . . . . . . . . . . 15 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
7371, 72ax-mp 5 . . . . . . . . . . . . . 14 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
74 ssid 3757 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ⊆ (𝐹𝑥)
7559ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → Fun 𝐹)
76 cnvimass 5635 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑥) ⊆ dom 𝐹
77 funimass3 6488 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ↔ (𝐹𝑥) ⊆ (𝐹𝑥)))
7875, 76, 77sylancl 697 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ↔ (𝐹𝑥) ⊆ (𝐹𝑥)))
7974, 78mpbiri 248 . . . . . . . . . . . . . . . . . . . 20 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ⊆ 𝑥)
80 imassrn 5627 . . . . . . . . . . . . . . . . . . . 20 (𝐹 “ (𝐹𝑥)) ⊆ ran 𝐹
81 ssin 3970 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ∧ (𝐹 “ (𝐹𝑥)) ⊆ ran 𝐹) ↔ (𝐹 “ (𝐹𝑥)) ⊆ (𝑥 ∩ ran 𝐹))
8279, 80, 81sylanblc 699 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ⊆ (𝑥 ∩ ran 𝐹))
83 elin 3931 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑧𝑥𝑧 ∈ ran 𝐹))
84 fvelrnb 6397 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 Fn 𝑌 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8511, 84syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹:𝑌𝑋 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
86853ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8786ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8875ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → Fun 𝐹)
8988, 76jctir 562 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → (Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹))
9059ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → Fun 𝐹)
9190ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → Fun 𝐹)
92473ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → dom 𝐹 = 𝑌)
9392ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → dom 𝐹 = 𝑌)
9493eleq2d 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑦 ∈ dom 𝐹𝑦𝑌))
9594biimpar 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → 𝑦 ∈ dom 𝐹)
96 fvimacnv 6487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
9791, 95, 96syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
9897biimpa 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → 𝑦 ∈ (𝐹𝑥))
99 funfvima2 6648 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → (𝑦 ∈ (𝐹𝑥) → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))))
10089, 98, 99sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥)))
101100ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))))
102 eleq1 2819 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ 𝑥𝑧𝑥))
103 eleq1 2819 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥)) ↔ 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
104102, 103imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹𝑦) = 𝑧 → (((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))) ↔ (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
105101, 104syl5ibcom 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) = 𝑧 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
106105rexlimdva 3161 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (∃𝑦𝑌 (𝐹𝑦) = 𝑧 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
10787, 106sylbid 230 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ ran 𝐹 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
108107com23 86 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧𝑥 → (𝑧 ∈ ran 𝐹𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
109108impd 446 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝑧𝑥𝑧 ∈ ran 𝐹) → 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
11083, 109syl5bi 232 . . . . . . . . . . . . . . . . . . . 20 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ (𝑥 ∩ ran 𝐹) → 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
111110ssrdv 3742 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ (𝐹 “ (𝐹𝑥)))
11282, 111eqssd 3753 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) = (𝑥 ∩ ran 𝐹))
113 filin 21851 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
1141133exp 1112 . . . . . . . . . . . . . . . . . . . . . 22 (𝐿 ∈ (Fil‘𝑋) → (𝑥𝐿 → (ran 𝐹𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
115114com23 86 . . . . . . . . . . . . . . . . . . . . 21 (𝐿 ∈ (Fil‘𝑋) → (ran 𝐹𝐿 → (𝑥𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
1161153ad2ant2 1128 . . . . . . . . . . . . . . . . . . . 20 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (ran 𝐹𝐿 → (𝑥𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
117116imp31 447 . . . . . . . . . . . . . . . . . . 19 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
118117adantr 472 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
119112, 118eqeltrd 2831 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)
120119exp32 632 . . . . . . . . . . . . . . . 16 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)))
121 imaeq2 5612 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝐹𝑥) → (𝐹𝑠) = (𝐹 “ (𝐹𝑥)))
122121sseq1d 3765 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡))
123121eleq1d 2816 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ∈ 𝐿 ↔ (𝐹 “ (𝐹𝑥)) ∈ 𝐿))
124123imbi2d 329 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐹𝑥) → ((𝑡𝑋 → (𝐹𝑠) ∈ 𝐿) ↔ (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)))
125122, 124imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐹𝑥) → (((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿)) ↔ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿))))
126120, 125syl5ibrcom 237 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
127126rexlimdva 3161 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
12873, 127syl5bi 232 . . . . . . . . . . . . 13 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
129128imp44 623 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → (𝐹𝑠) ∈ 𝐿)
130 simprr 813 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝑡𝑋)
131 simprlr 822 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → (𝐹𝑠) ⊆ 𝑡)
132 filss 21850 . . . . . . . . . . . 12 ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝐹𝑠) ∈ 𝐿𝑡𝑋 ∧ (𝐹𝑠) ⊆ 𝑡)) → 𝑡𝐿)
13370, 129, 130, 131, 132syl13anc 1475 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝑡𝐿)
134133exp44 642 . . . . . . . . . 10 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
135134rexlimdv 3160 . . . . . . . . 9 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
136135com23 86 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝑋 → (∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡𝑡𝐿)))
137136impd 446 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡) → 𝑡𝐿))
13869, 137impbid 202 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
1392adantr 472 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑋𝐿)
140 rnelfmlem 21949 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
141 simpl3 1229 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐹:𝑌𝑋)
142 elfm 21944 . . . . . . 7 ((𝑋𝐿 ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
143139, 140, 141, 142syl3anc 1473 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
144138, 143bitr4d 271 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥)))))
145144eqrdv 2750 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 = ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))))
1468adantr 472 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌))
147 fnfvelrn 6511 . . . . 5 (((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ ran (𝑋 FilMap 𝐹))
148146, 140, 147syl2anc 696 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ ran (𝑋 FilMap 𝐹))
149145, 148eqeltrd 2831 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 ∈ ran (𝑋 FilMap 𝐹))
150149ex 449 . 2 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (ran 𝐹𝐿𝐿 ∈ ran (𝑋 FilMap 𝐹)))
15134, 150impbid 202 1 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ran 𝐹𝐿))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1624  wcel 2131  wrex 3043  Vcvv 3332  cin 3706  wss 3707  cmpt 4873  ccnv 5257  dom cdm 5258  ran crn 5259  cima 5261  Fun wfun 6035   Fn wfn 6036  wf 6037  ontowfo 6039  cfv 6041  (class class class)co 6805  fBascfbas 19928  filGencfg 19929  Filcfil 21842   FilMap cfm 21930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-fbas 19937  df-fg 19938  df-fil 21843  df-fm 21935
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator