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

Theorem rnelfm 21966
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 21868 . . . . . . 7 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
213ad2ant2 1157 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑋𝐿)
3 simp1 1159 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑌𝐴)
4 simp3 1161 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝐹:𝑌𝑋)
5 fmf 21958 . . . . . 6 ((𝑋𝐿𝑌𝐴𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
62, 3, 4, 5syl3anc 1483 . . . . 5 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
76ffnd 6253 . . . 4 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌))
8 fvelrnb 6460 . . . 4 ((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿))
97, 8syl 17 . . 3 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿))
10 ffn 6252 . . . . . . . . . . . 12 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
11 dffn4 6333 . . . . . . . . . . . 12 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
1210, 11sylib 209 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
13 foima 6332 . . . . . . . . . . 11 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
1412, 13syl 17 . . . . . . . . . 10 (𝐹:𝑌𝑋 → (𝐹𝑌) = ran 𝐹)
1514ad2antlr 709 . . . . . . . . 9 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹𝑌) = ran 𝐹)
16 simpll 774 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑋𝐿)
17 simpr 473 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑏 ∈ (fBas‘𝑌))
18 simplr 776 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝐹:𝑌𝑋)
19 fgcl 21891 . . . . . . . . . . . 12 (𝑏 ∈ (fBas‘𝑌) → (𝑌filGen𝑏) ∈ (Fil‘𝑌))
20 filtop 21868 . . . . . . . . . . . 12 ((𝑌filGen𝑏) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏))
2119, 20syl 17 . . . . . . . . . . 11 (𝑏 ∈ (fBas‘𝑌) → 𝑌 ∈ (𝑌filGen𝑏))
2221adantl 469 . . . . . . . . . 10 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → 𝑌 ∈ (𝑌filGen𝑏))
23 eqid 2806 . . . . . . . . . . 11 (𝑌filGen𝑏) = (𝑌filGen𝑏)
2423imaelfm 21964 . . . . . . . . . 10 (((𝑋𝐿𝑏 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝑏)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏))
2516, 17, 18, 22, 24syl31anc 1485 . . . . . . . . 9 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝑏))
2615, 25eqeltrrd 2886 . . . . . . . 8 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏))
27 eleq2 2874 . . . . . . . 8 (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → (ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝑏) ↔ ran 𝐹𝐿))
2826, 27syl5ibcom 236 . . . . . . 7 (((𝑋𝐿𝐹:𝑌𝑋) ∧ 𝑏 ∈ (fBas‘𝑌)) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿))
2928ex 399 . . . . . 6 ((𝑋𝐿𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
301, 29sylan 571 . . . . 5 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
31303adant1 1153 . . . 4 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) → (((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿)))
3231rexlimdv 3218 . . 3 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (∃𝑏 ∈ (fBas‘𝑌)((𝑋 FilMap 𝐹)‘𝑏) = 𝐿 → ran 𝐹𝐿))
339, 32sylbid 231 . 2 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) → ran 𝐹𝐿))
34 simpl2 1237 . . . . . . . . 9 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 ∈ (Fil‘𝑋))
35 filelss 21865 . . . . . . . . . 10 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡𝐿) → 𝑡𝑋)
3635ex 399 . . . . . . . . 9 (𝐿 ∈ (Fil‘𝑋) → (𝑡𝐿𝑡𝑋))
3734, 36syl 17 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿𝑡𝑋))
38 simpr 473 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → 𝑡𝐿)
39 eqidd 2807 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹𝑡) = (𝐹𝑡))
40 imaeq2 5672 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
4140rspceeqv 3520 . . . . . . . . . . . 12 ((𝑡𝐿 ∧ (𝐹𝑡) = (𝐹𝑡)) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
4238, 39, 41syl2anc 575 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥))
43 simpl1 1235 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌𝐴)
44 cnvimass 5695 . . . . . . . . . . . . . . . . 17 (𝐹𝑡) ⊆ dom 𝐹
45 fdm 6260 . . . . . . . . . . . . . . . . 17 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
4644, 45syl5sseq 3850 . . . . . . . . . . . . . . . 16 (𝐹:𝑌𝑋 → (𝐹𝑡) ⊆ 𝑌)
47463ad2ant3 1158 . . . . . . . . . . . . . . 15 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹𝑡) ⊆ 𝑌)
4847adantr 468 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑡) ⊆ 𝑌)
4943, 48ssexd 5000 . . . . . . . . . . . . 13 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑡) ∈ V)
50 eqid 2806 . . . . . . . . . . . . . 14 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
5150elrnmpt 5573 . . . . . . . . . . . . 13 ((𝐹𝑡) ∈ V → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5249, 51syl 17 . . . . . . . . . . . 12 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5352adantr 468 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹𝑡) = (𝐹𝑥)))
5442, 53mpbird 248 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
55 ssid 3820 . . . . . . . . . . 11 (𝐹𝑡) ⊆ (𝐹𝑡)
56 ffun 6255 . . . . . . . . . . . . . 14 (𝐹:𝑌𝑋 → Fun 𝐹)
57563ad2ant3 1158 . . . . . . . . . . . . 13 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → Fun 𝐹)
5857ad2antrr 708 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → Fun 𝐹)
59 funimass3 6551 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ (𝐹𝑡) ⊆ dom 𝐹) → ((𝐹 “ (𝐹𝑡)) ⊆ 𝑡 ↔ (𝐹𝑡) ⊆ (𝐹𝑡)))
6058, 44, 59sylancl 576 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ((𝐹 “ (𝐹𝑡)) ⊆ 𝑡 ↔ (𝐹𝑡) ⊆ (𝐹𝑡)))
6155, 60mpbiri 249 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → (𝐹 “ (𝐹𝑡)) ⊆ 𝑡)
62 imaeq2 5672 . . . . . . . . . . . 12 (𝑠 = (𝐹𝑡) → (𝐹𝑠) = (𝐹 “ (𝐹𝑡)))
6362sseq1d 3829 . . . . . . . . . . 11 (𝑠 = (𝐹𝑡) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡))
6463rspcev 3502 . . . . . . . . . 10 (((𝐹𝑡) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹 “ (𝐹𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)
6554, 61, 64syl2anc 575 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑡𝐿) → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)
6665ex 399 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 → ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡))
6737, 66jcad 504 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 → (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
6834adantr 468 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝐿 ∈ (Fil‘𝑋))
69 vex 3394 . . . . . . . . . . . . . . 15 𝑠 ∈ V
7050elrnmpt 5573 . . . . . . . . . . . . . . 15 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
7169, 70ax-mp 5 . . . . . . . . . . . . . 14 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
72 ssid 3820 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ⊆ (𝐹𝑥)
7357ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → Fun 𝐹)
74 cnvimass 5695 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑥) ⊆ dom 𝐹
75 funimass3 6551 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ↔ (𝐹𝑥) ⊆ (𝐹𝑥)))
7673, 74, 75sylancl 576 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ↔ (𝐹𝑥) ⊆ (𝐹𝑥)))
7772, 76mpbiri 249 . . . . . . . . . . . . . . . . . . . 20 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ⊆ 𝑥)
78 imassrn 5687 . . . . . . . . . . . . . . . . . . . 20 (𝐹 “ (𝐹𝑥)) ⊆ ran 𝐹
79 ssin 4031 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 “ (𝐹𝑥)) ⊆ 𝑥 ∧ (𝐹 “ (𝐹𝑥)) ⊆ ran 𝐹) ↔ (𝐹 “ (𝐹𝑥)) ⊆ (𝑥 ∩ ran 𝐹))
8077, 78, 79sylanblc 579 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ⊆ (𝑥 ∩ ran 𝐹))
81 elin 3995 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑧𝑥𝑧 ∈ ran 𝐹))
82 fvelrnb 6460 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 Fn 𝑌 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8310, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹:𝑌𝑋 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
84833ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8584ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑦𝑌 (𝐹𝑦) = 𝑧))
8673ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → Fun 𝐹)
8786, 74jctir 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → (Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹))
8857ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → Fun 𝐹)
8988ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → Fun 𝐹)
90453ad2ant3 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → dom 𝐹 = 𝑌)
9190ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → dom 𝐹 = 𝑌)
9291eleq2d 2871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑦 ∈ dom 𝐹𝑦𝑌))
9392biimpar 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → 𝑦 ∈ dom 𝐹)
94 fvimacnv 6550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
9589, 93, 94syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
9695biimpa 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → 𝑦 ∈ (𝐹𝑥))
97 funfvima2 6714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun 𝐹 ∧ (𝐹𝑥) ⊆ dom 𝐹) → (𝑦 ∈ (𝐹𝑥) → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))))
9887, 96, 97sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) ∧ (𝐹𝑦) ∈ 𝑥) → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥)))
9998ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))))
100 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ 𝑥𝑧𝑥))
101 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑦) = 𝑧 → ((𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥)) ↔ 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
102100, 101imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹𝑦) = 𝑧 → (((𝐹𝑦) ∈ 𝑥 → (𝐹𝑦) ∈ (𝐹 “ (𝐹𝑥))) ↔ (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
10399, 102syl5ibcom 236 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) ∧ 𝑦𝑌) → ((𝐹𝑦) = 𝑧 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
104103rexlimdva 3219 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (∃𝑦𝑌 (𝐹𝑦) = 𝑧 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
10585, 104sylbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ ran 𝐹 → (𝑧𝑥𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
106105com23 86 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧𝑥 → (𝑧 ∈ ran 𝐹𝑧 ∈ (𝐹 “ (𝐹𝑥)))))
107106impd 398 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → ((𝑧𝑥𝑧 ∈ ran 𝐹) → 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
10881, 107syl5bi 233 . . . . . . . . . . . . . . . . . . . 20 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑧 ∈ (𝑥 ∩ ran 𝐹) → 𝑧 ∈ (𝐹 “ (𝐹𝑥))))
109108ssrdv 3804 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ (𝐹 “ (𝐹𝑥)))
11080, 109eqssd 3815 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) = (𝑥 ∩ ran 𝐹))
111 filin 21867 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
1121113exp 1141 . . . . . . . . . . . . . . . . . . . . . 22 (𝐿 ∈ (Fil‘𝑋) → (𝑥𝐿 → (ran 𝐹𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
113112com23 86 . . . . . . . . . . . . . . . . . . . . 21 (𝐿 ∈ (Fil‘𝑋) → (ran 𝐹𝐿 → (𝑥𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
1141133ad2ant2 1157 . . . . . . . . . . . . . . . . . . . 20 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (ran 𝐹𝐿 → (𝑥𝐿 → (𝑥 ∩ ran 𝐹) ∈ 𝐿)))
115114imp31 406 . . . . . . . . . . . . . . . . . . 19 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
116115adantr 468 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
117110, 116eqeltrd 2885 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) ∧ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡𝑡𝑋)) → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)
118117exp32 409 . . . . . . . . . . . . . . . 16 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)))
119 imaeq2 5672 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝐹𝑥) → (𝐹𝑠) = (𝐹 “ (𝐹𝑥)))
120119sseq1d 3829 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝐹𝑥)) ⊆ 𝑡))
121119eleq1d 2870 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ∈ 𝐿 ↔ (𝐹 “ (𝐹𝑥)) ∈ 𝐿))
122121imbi2d 331 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐹𝑥) → ((𝑡𝑋 → (𝐹𝑠) ∈ 𝐿) ↔ (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿)))
123120, 122imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐹𝑥) → (((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿)) ↔ ((𝐹 “ (𝐹𝑥)) ⊆ 𝑡 → (𝑡𝑋 → (𝐹 “ (𝐹𝑥)) ∈ 𝐿))))
124118, 123syl5ibrcom 238 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
125124rexlimdva 3219 . . . . . . . . . . . . . 14 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑥𝐿 𝑠 = (𝐹𝑥) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
12671, 125syl5bi 233 . . . . . . . . . . . . 13 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋 → (𝐹𝑠) ∈ 𝐿))))
127126imp44 417 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → (𝐹𝑠) ∈ 𝐿)
128 simprr 780 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝑡𝑋)
129 simprlr 789 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → (𝐹𝑠) ⊆ 𝑡)
130 filss 21866 . . . . . . . . . . . 12 ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝐹𝑠) ∈ 𝐿𝑡𝑋 ∧ (𝐹𝑠) ⊆ 𝑡)) → 𝑡𝐿)
13168, 127, 128, 129, 130syl13anc 1484 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹𝑠) ⊆ 𝑡) ∧ 𝑡𝑋)) → 𝑡𝐿)
132131exp44 426 . . . . . . . . . 10 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ((𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿))))
133132rexlimdv 3218 . . . . . . . . 9 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡 → (𝑡𝑋𝑡𝐿)))
134133com23 86 . . . . . . . 8 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝑋 → (∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡𝑡𝐿)))
135134impd 398 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡) → 𝑡𝐿))
13667, 135impbid 203 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
1372adantr 468 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑋𝐿)
138 rnelfmlem 21965 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
139 simpl3 1239 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐹:𝑌𝑋)
140 elfm 21960 . . . . . . 7 ((𝑋𝐿 ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
141137, 138, 139, 140syl3anc 1483 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝐹𝑠) ⊆ 𝑡)))
142136, 141bitr4d 273 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑡𝐿𝑡 ∈ ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥)))))
143142eqrdv 2804 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 = ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))))
1447adantr 468 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑋 FilMap 𝐹) Fn (fBas‘𝑌))
145 fnfvelrn 6574 . . . . 5 (((𝑋 FilMap 𝐹) Fn (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ ran (𝑋 FilMap 𝐹))
146144, 138, 145syl2anc 575 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑋 FilMap 𝐹)‘ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ ran (𝑋 FilMap 𝐹))
147143, 146eqeltrd 2885 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐿 ∈ ran (𝑋 FilMap 𝐹))
148147ex 399 . 2 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (ran 𝐹𝐿𝐿 ∈ ran (𝑋 FilMap 𝐹)))
14933, 148impbid 203 1 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ran 𝐹𝐿))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wrex 3097  Vcvv 3391  cin 3768  wss 3769  cmpt 4923  ccnv 5310  dom cdm 5311  ran crn 5312  cima 5314  Fun wfun 6091   Fn wfn 6092  wf 6093  ontowfo 6095  cfv 6097  (class class class)co 6870  fBascfbas 19938  filGencfg 19939  Filcfil 21858   FilMap cfm 21946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-fbas 19947  df-fg 19948  df-fil 21859  df-fm 21951
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator