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

Theorem rnelfmlem 23209
Description: Lemma for rnelfm 23210. (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 1191 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌𝐴)
2 cnvimass 6024 . . . . . . 7 (𝐹𝑥) ⊆ dom 𝐹
3 simpl3 1193 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐹:𝑌𝑋)
42, 3fssdm 6676 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ⊆ 𝑌)
51, 4sselpwd 5275 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
65adantr 482 . . . 4 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
76fmpttd 7050 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑥𝐿 ↦ (𝐹𝑥)):𝐿⟶𝒫 𝑌)
87frnd 6664 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
9 filtop 23112 . . . . . . . 8 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
1093ad2ant2 1134 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑋𝐿)
1110adantr 482 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑋𝐿)
12 fimacnv 6678 . . . . . . . . 9 (𝐹:𝑌𝑋 → (𝐹𝑋) = 𝑌)
1312eqcomd 2743 . . . . . . . 8 (𝐹:𝑌𝑋𝑌 = (𝐹𝑋))
14133ad2ant3 1135 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑌 = (𝐹𝑋))
1514adantr 482 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 = (𝐹𝑋))
16 imaeq2 6000 . . . . . . 7 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
1716rspceeqv 3588 . . . . . 6 ((𝑋𝐿𝑌 = (𝐹𝑋)) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
1811, 15, 17syl2anc 585 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
19 eqid 2737 . . . . . . . 8 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
2019elrnmpt 5902 . . . . . . 7 (𝑌𝐴 → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
21203ad2ant1 1133 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2221adantr 482 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2318, 22mpbird 257 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
2423ne0d 4287 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅)
25 0nelfil 23106 . . . . . . 7 (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
26253ad2ant2 1134 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → ¬ ∅ ∈ 𝐿)
2726adantr 482 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ 𝐿)
28 0ex 5256 . . . . . . 7 ∅ ∈ V
2919elrnmpt 5902 . . . . . . 7 (∅ ∈ V → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥)))
3028, 29ax-mp 5 . . . . . 6 (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥))
31 ffn 6656 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
32 fvelrnb 6891 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3331, 32syl 17 . . . . . . . . . . . . . . . . 17 (𝐹:𝑌𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
34333ad2ant3 1135 . . . . . . . . . . . . . . . 16 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3534ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
36 eleq1 2825 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑧) = 𝑦 → ((𝐹𝑧) ∈ 𝑥𝑦𝑥))
3736biimparc 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥 ∧ (𝐹𝑧) = 𝑦) → (𝐹𝑧) ∈ 𝑥)
3837ad2ant2l 744 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐿𝑦𝑥) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
3938adantll 712 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
40 ffun 6659 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:𝑌𝑋 → Fun 𝐹)
41403ad2ant3 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → Fun 𝐹)
4241ad3antrrr 728 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → Fun 𝐹)
43 fdm 6665 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
4443eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝑌𝑋 → (𝑧 ∈ dom 𝐹𝑧𝑌))
4544biimpar 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝑌𝑋𝑧𝑌) → 𝑧 ∈ dom 𝐹)
46453ad2antl3 1187 . . . . . . . . . . . . . . . . . . . . 21 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
4746adantlr 713 . . . . . . . . . . . . . . . . . . . 20 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
4847ad2ant2r 745 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
49 fvimacnv 6991 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5042, 48, 49syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5139, 50mpbid 231 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ (𝐹𝑥))
52 n0i 4285 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝐹𝑥) → ¬ (𝐹𝑥) = ∅)
53 eqcom 2744 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = ∅ ↔ ∅ = (𝐹𝑥))
5452, 53sylnib 328 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐹𝑥) → ¬ ∅ = (𝐹𝑥))
5551, 54syl 17 . . . . . . . . . . . . . . . 16 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ¬ ∅ = (𝐹𝑥))
5655rexlimdvaa 3150 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∃𝑧𝑌 (𝐹𝑧) = 𝑦 → ¬ ∅ = (𝐹𝑥)))
5735, 56sylbid 239 . . . . . . . . . . . . . 14 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (𝐹𝑥)))
5857con2d 134 . . . . . . . . . . . . 13 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹))
5958expr 458 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑦𝑥 → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
6059com23 86 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (∅ = (𝐹𝑥) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
6160impr 456 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
6261alrimiv 1930 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
63 imnan 401 . . . . . . . . . . . 12 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦𝑥𝑦 ∈ ran 𝐹))
64 elin 3918 . . . . . . . . . . . 12 (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦𝑥𝑦 ∈ ran 𝐹))
6563, 64xchbinxr 335 . . . . . . . . . . 11 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
6665albii 1821 . . . . . . . . . 10 (∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
67 eq0 4295 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
68 eqcom 2744 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
6966, 67, 683bitr2i 299 . . . . . . . . 9 (∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∅ = (𝑥 ∩ ran 𝐹))
7062, 69sylib 217 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∅ = (𝑥 ∩ ran 𝐹))
71 simpll2 1213 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → 𝐿 ∈ (Fil‘𝑋))
72 simprl 769 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → 𝑥𝐿)
73 simplr 767 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ran 𝐹𝐿)
74 filin 23111 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7571, 72, 73, 74syl3anc 1371 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7670, 75eqeltrd 2838 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∅ ∈ 𝐿)
7776rexlimdvaa 3150 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑥𝐿 ∅ = (𝐹𝑥) → ∅ ∈ 𝐿))
7830, 77biimtrid 241 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ∅ ∈ 𝐿))
7927, 78mtod 197 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
80 df-nel 3048 . . . 4 (∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
8179, 80sylibr 233 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)))
8219elrnmpt 5902 . . . . . . . . 9 (𝑟 ∈ V → (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥)))
8382elv 3448 . . . . . . . 8 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥))
84 imaeq2 6000 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝐹𝑥) = (𝐹𝑢))
8584eqeq2d 2748 . . . . . . . . 9 (𝑥 = 𝑢 → (𝑟 = (𝐹𝑥) ↔ 𝑟 = (𝐹𝑢)))
8685cbvrexvw 3223 . . . . . . . 8 (∃𝑥𝐿 𝑟 = (𝐹𝑥) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
8783, 86bitri 275 . . . . . . 7 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
8819elrnmpt 5902 . . . . . . . . 9 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
8988elv 3448 . . . . . . . 8 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
90 imaeq2 6000 . . . . . . . . . 10 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
9190eqeq2d 2748 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑠 = (𝐹𝑥) ↔ 𝑠 = (𝐹𝑣)))
9291cbvrexvw 3223 . . . . . . . 8 (∃𝑥𝐿 𝑠 = (𝐹𝑥) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9389, 92bitri 275 . . . . . . 7 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9487, 93anbi12i 628 . . . . . 6 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
95 reeanv 3214 . . . . . 6 (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
9694, 95bitr4i 278 . . . . 5 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))
97 filin 23111 . . . . . . . . . . . . . 14 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢𝐿𝑣𝐿) → (𝑢𝑣) ∈ 𝐿)
98973expb 1120 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
9998adantlr 713 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
100 eqidd 2738 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣)))
101 imaeq2 6000 . . . . . . . . . . . . 13 (𝑥 = (𝑢𝑣) → (𝐹𝑥) = (𝐹 “ (𝑢𝑣)))
102101rspceeqv 3588 . . . . . . . . . . . 12 (((𝑢𝑣) ∈ 𝐿 ∧ (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
10399, 100, 102syl2anc 585 . . . . . . . . . . 11 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
1041033adantl1 1166 . . . . . . . . . 10 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
105104ad2ant2r 745 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
106 simpll1 1212 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑌𝐴)
107 cnvimass 6024 . . . . . . . . . . . . . 14 (𝐹 “ (𝑢𝑣)) ⊆ dom 𝐹
108107, 43sseqtrid 3988 . . . . . . . . . . . . 13 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
1091083ad2ant3 1135 . . . . . . . . . . . 12 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
110109ad2antrr 724 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
111106, 110ssexd 5273 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ V)
11219elrnmpt 5902 . . . . . . . . . 10 ((𝐹 “ (𝑢𝑣)) ∈ V → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
113111, 112syl 17 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
114105, 113mpbird 257 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
115 simprrl 779 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑟 = (𝐹𝑢))
116 simprrr 780 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑠 = (𝐹𝑣))
117115, 116ineq12d 4165 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = ((𝐹𝑢) ∩ (𝐹𝑣)))
118 funcnvcnv 6556 . . . . . . . . . . . . 13 (Fun 𝐹 → Fun 𝐹)
119 imain 6574 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
12040, 118, 1193syl 18 . . . . . . . . . . . 12 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
1211203ad2ant3 1135 . . . . . . . . . . 11 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
122121ad2antrr 724 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
123117, 122eqtr4d 2780 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = (𝐹 “ (𝑢𝑣)))
124 eqimss2 3993 . . . . . . . . 9 ((𝑟𝑠) = (𝐹 “ (𝑢𝑣)) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
125123, 124syl 17 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
126 sseq1 3961 . . . . . . . . 9 (𝑡 = (𝐹 “ (𝑢𝑣)) → (𝑡 ⊆ (𝑟𝑠) ↔ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)))
127126rspcev 3574 . . . . . . . 8 (((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
128114, 125, 127syl2anc 585 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
129128exp32 422 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑢𝐿𝑣𝐿) → ((𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))))
130129rexlimdvv 3201 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
13196, 130biimtrid 241 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
132131ralrimivv 3192 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
13324, 81, 1323jca 1128 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
134 isfbas2 23092 . . 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 711 1 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1087  wal 1539   = wceq 1541  wcel 2106  wne 2941  wnel 3047  wral 3062  wrex 3071  Vcvv 3442  cin 3901  wss 3902  c0 4274  𝒫 cpw 4552  cmpt 5180  ccnv 5624  dom cdm 5625  ran crn 5626  cima 5628  Fun wfun 6478   Fn wfn 6479  wf 6480  cfv 6484  fBascfbas 20691  Filcfil 23102
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-br 5098  df-opab 5160  df-mpt 5181  df-id 5523  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-fv 6492  df-fbas 20700  df-fil 23103
This theorem is referenced by:  rnelfm  23210  fmfnfm  23215
  Copyright terms: Public domain W3C validator