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

Theorem rnelfmlem 22557
 Description: Lemma for rnelfm 22558. (Contributed by Jeff Hankins, 14-Nov-2009.)
Assertion
Ref Expression
rnelfmlem (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐿   𝑥,𝑋   𝑥,𝑌

Proof of Theorem rnelfmlem
Dummy variables 𝑟 𝑠 𝑡 𝑢 𝑣 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl1 1188 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌𝐴)
2 cnvimass 5916 . . . . . . 7 (𝐹𝑥) ⊆ dom 𝐹
3 simpl3 1190 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐹:𝑌𝑋)
42, 3fssdm 6504 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ⊆ 𝑌)
51, 4sselpwd 5194 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
65adantr 484 . . . 4 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
76fmpttd 6856 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑥𝐿 ↦ (𝐹𝑥)):𝐿⟶𝒫 𝑌)
87frnd 6494 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
9 filtop 22460 . . . . . . . 8 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
1093ad2ant2 1131 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑋𝐿)
1110adantr 484 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑋𝐿)
12 fimacnv 6816 . . . . . . . . 9 (𝐹:𝑌𝑋 → (𝐹𝑋) = 𝑌)
1312eqcomd 2804 . . . . . . . 8 (𝐹:𝑌𝑋𝑌 = (𝐹𝑋))
14133ad2ant3 1132 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑌 = (𝐹𝑋))
1514adantr 484 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 = (𝐹𝑋))
16 imaeq2 5892 . . . . . . 7 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
1716rspceeqv 3586 . . . . . 6 ((𝑋𝐿𝑌 = (𝐹𝑋)) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
1811, 15, 17syl2anc 587 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
19 eqid 2798 . . . . . . . 8 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
2019elrnmpt 5792 . . . . . . 7 (𝑌𝐴 → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
21203ad2ant1 1130 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2221adantr 484 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2318, 22mpbird 260 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
2423ne0d 4251 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅)
25 0nelfil 22454 . . . . . . 7 (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
26253ad2ant2 1131 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → ¬ ∅ ∈ 𝐿)
2726adantr 484 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ 𝐿)
28 0ex 5175 . . . . . . 7 ∅ ∈ V
2919elrnmpt 5792 . . . . . . 7 (∅ ∈ V → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥)))
3028, 29ax-mp 5 . . . . . 6 (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥))
31 ffn 6487 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
32 fvelrnb 6701 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3331, 32syl 17 . . . . . . . . . . . . . . . . 17 (𝐹:𝑌𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
34333ad2ant3 1132 . . . . . . . . . . . . . . . 16 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3534ad2antrr 725 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
36 eleq1 2877 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑧) = 𝑦 → ((𝐹𝑧) ∈ 𝑥𝑦𝑥))
3736biimparc 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥 ∧ (𝐹𝑧) = 𝑦) → (𝐹𝑧) ∈ 𝑥)
3837ad2ant2l 745 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐿𝑦𝑥) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
3938adantll 713 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
40 ffun 6490 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:𝑌𝑋 → Fun 𝐹)
41403ad2ant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → Fun 𝐹)
4241ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → Fun 𝐹)
43 fdm 6495 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
4443eleq2d 2875 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝑌𝑋 → (𝑧 ∈ dom 𝐹𝑧𝑌))
4544biimpar 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝑌𝑋𝑧𝑌) → 𝑧 ∈ dom 𝐹)
46453ad2antl3 1184 . . . . . . . . . . . . . . . . . . . . 21 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
4746adantlr 714 . . . . . . . . . . . . . . . . . . . 20 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
4847ad2ant2r 746 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
49 fvimacnv 6800 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5042, 48, 49syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5139, 50mpbid 235 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ (𝐹𝑥))
52 n0i 4249 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝐹𝑥) → ¬ (𝐹𝑥) = ∅)
53 eqcom 2805 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = ∅ ↔ ∅ = (𝐹𝑥))
5452, 53sylnib 331 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐹𝑥) → ¬ ∅ = (𝐹𝑥))
5551, 54syl 17 . . . . . . . . . . . . . . . 16 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ¬ ∅ = (𝐹𝑥))
5655rexlimdvaa 3244 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∃𝑧𝑌 (𝐹𝑧) = 𝑦 → ¬ ∅ = (𝐹𝑥)))
5735, 56sylbid 243 . . . . . . . . . . . . . 14 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (𝐹𝑥)))
5857con2d 136 . . . . . . . . . . . . 13 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹))
5958expr 460 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑦𝑥 → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
6059com23 86 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (∅ = (𝐹𝑥) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
6160impr 458 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
6261alrimiv 1928 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
63 imnan 403 . . . . . . . . . . . 12 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦𝑥𝑦 ∈ ran 𝐹))
64 elin 3897 . . . . . . . . . . . 12 (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦𝑥𝑦 ∈ ran 𝐹))
6563, 64xchbinxr 338 . . . . . . . . . . 11 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
6665albii 1821 . . . . . . . . . 10 (∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
67 eq0 4258 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
68 eqcom 2805 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
6966, 67, 683bitr2i 302 . . . . . . . . 9 (∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∅ = (𝑥 ∩ ran 𝐹))
7062, 69sylib 221 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∅ = (𝑥 ∩ ran 𝐹))
71 simpll2 1210 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → 𝐿 ∈ (Fil‘𝑋))
72 simprl 770 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → 𝑥𝐿)
73 simplr 768 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ran 𝐹𝐿)
74 filin 22459 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7571, 72, 73, 74syl3anc 1368 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7670, 75eqeltrd 2890 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∅ ∈ 𝐿)
7776rexlimdvaa 3244 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑥𝐿 ∅ = (𝐹𝑥) → ∅ ∈ 𝐿))
7830, 77syl5bi 245 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ∅ ∈ 𝐿))
7927, 78mtod 201 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
80 df-nel 3092 . . . 4 (∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
8179, 80sylibr 237 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)))
8219elrnmpt 5792 . . . . . . . . 9 (𝑟 ∈ V → (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥)))
8382elv 3446 . . . . . . . 8 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥))
84 imaeq2 5892 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝐹𝑥) = (𝐹𝑢))
8584eqeq2d 2809 . . . . . . . . 9 (𝑥 = 𝑢 → (𝑟 = (𝐹𝑥) ↔ 𝑟 = (𝐹𝑢)))
8685cbvrexvw 3397 . . . . . . . 8 (∃𝑥𝐿 𝑟 = (𝐹𝑥) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
8783, 86bitri 278 . . . . . . 7 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
8819elrnmpt 5792 . . . . . . . . 9 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
8988elv 3446 . . . . . . . 8 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
90 imaeq2 5892 . . . . . . . . . 10 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
9190eqeq2d 2809 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑠 = (𝐹𝑥) ↔ 𝑠 = (𝐹𝑣)))
9291cbvrexvw 3397 . . . . . . . 8 (∃𝑥𝐿 𝑠 = (𝐹𝑥) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9389, 92bitri 278 . . . . . . 7 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9487, 93anbi12i 629 . . . . . 6 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
95 reeanv 3320 . . . . . 6 (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
9694, 95bitr4i 281 . . . . 5 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))
97 filin 22459 . . . . . . . . . . . . . 14 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢𝐿𝑣𝐿) → (𝑢𝑣) ∈ 𝐿)
98973expb 1117 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
9998adantlr 714 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
100 eqidd 2799 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣)))
101 imaeq2 5892 . . . . . . . . . . . . 13 (𝑥 = (𝑢𝑣) → (𝐹𝑥) = (𝐹 “ (𝑢𝑣)))
102101rspceeqv 3586 . . . . . . . . . . . 12 (((𝑢𝑣) ∈ 𝐿 ∧ (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
10399, 100, 102syl2anc 587 . . . . . . . . . . 11 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
1041033adantl1 1163 . . . . . . . . . 10 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
105104ad2ant2r 746 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
106 simpll1 1209 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑌𝐴)
107 cnvimass 5916 . . . . . . . . . . . . . 14 (𝐹 “ (𝑢𝑣)) ⊆ dom 𝐹
108107, 43sseqtrid 3967 . . . . . . . . . . . . 13 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
1091083ad2ant3 1132 . . . . . . . . . . . 12 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
110109ad2antrr 725 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
111106, 110ssexd 5192 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ V)
11219elrnmpt 5792 . . . . . . . . . 10 ((𝐹 “ (𝑢𝑣)) ∈ V → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
113111, 112syl 17 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
114105, 113mpbird 260 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
115 simprrl 780 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑟 = (𝐹𝑢))
116 simprrr 781 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑠 = (𝐹𝑣))
117115, 116ineq12d 4140 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = ((𝐹𝑢) ∩ (𝐹𝑣)))
118 funcnvcnv 6391 . . . . . . . . . . . . 13 (Fun 𝐹 → Fun 𝐹)
119 imain 6409 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
12040, 118, 1193syl 18 . . . . . . . . . . . 12 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
1211203ad2ant3 1132 . . . . . . . . . . 11 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
122121ad2antrr 725 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
123117, 122eqtr4d 2836 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = (𝐹 “ (𝑢𝑣)))
124 eqimss2 3972 . . . . . . . . 9 ((𝑟𝑠) = (𝐹 “ (𝑢𝑣)) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
125123, 124syl 17 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
126 sseq1 3940 . . . . . . . . 9 (𝑡 = (𝐹 “ (𝑢𝑣)) → (𝑡 ⊆ (𝑟𝑠) ↔ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)))
127126rspcev 3571 . . . . . . . 8 (((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
128114, 125, 127syl2anc 587 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
129128exp32 424 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑢𝐿𝑣𝐿) → ((𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))))
130129rexlimdvv 3252 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
13196, 130syl5bi 245 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
132131ralrimivv 3155 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
13324, 81, 1323jca 1125 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
134 isfbas2 22440 . . 3 (𝑌𝐴 → (ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))))
1351, 134syl 17 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))))
1368, 133, 135mpbir2and 712 1 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ≠ wne 2987   ∉ wnel 3091  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497   ↦ cmpt 5110  ◡ccnv 5518  dom cdm 5519  ran crn 5520   “ cima 5522  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  fBascfbas 20079  Filcfil 22450 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295 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 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-fbas 20088  df-fil 22451 This theorem is referenced by:  rnelfm  22558  fmfnfm  22563
 Copyright terms: Public domain W3C validator