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

Theorem rnelfmlem 23303
Description: Lemma for rnelfm 23304. (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 6033 . . . . . . 7 (𝐹𝑥) ⊆ dom 𝐹
3 simpl3 1193 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐹:𝑌𝑋)
42, 3fssdm 6688 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ⊆ 𝑌)
51, 4sselpwd 5283 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
65adantr 481 . . . 4 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
76fmpttd 7063 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑥𝐿 ↦ (𝐹𝑥)):𝐿⟶𝒫 𝑌)
87frnd 6676 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
9 filtop 23206 . . . . . . . 8 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
1093ad2ant2 1134 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑋𝐿)
1110adantr 481 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑋𝐿)
12 fimacnv 6690 . . . . . . . . 9 (𝐹:𝑌𝑋 → (𝐹𝑋) = 𝑌)
1312eqcomd 2742 . . . . . . . 8 (𝐹:𝑌𝑋𝑌 = (𝐹𝑋))
14133ad2ant3 1135 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑌 = (𝐹𝑋))
1514adantr 481 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 = (𝐹𝑋))
16 imaeq2 6009 . . . . . . 7 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
1716rspceeqv 3595 . . . . . 6 ((𝑋𝐿𝑌 = (𝐹𝑋)) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
1811, 15, 17syl2anc 584 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
19 eqid 2736 . . . . . . . 8 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
2019elrnmpt 5911 . . . . . . 7 (𝑌𝐴 → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
21203ad2ant1 1133 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2221adantr 481 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2318, 22mpbird 256 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
2423ne0d 4295 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅)
25 0nelfil 23200 . . . . . . 7 (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
26253ad2ant2 1134 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → ¬ ∅ ∈ 𝐿)
2726adantr 481 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ 𝐿)
28 0ex 5264 . . . . . . 7 ∅ ∈ V
2919elrnmpt 5911 . . . . . . 7 (∅ ∈ V → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥)))
3028, 29ax-mp 5 . . . . . 6 (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥))
31 ffn 6668 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
32 fvelrnb 6903 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3331, 32syl 17 . . . . . . . . . . . . . . . . 17 (𝐹:𝑌𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
34333ad2ant3 1135 . . . . . . . . . . . . . . . 16 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3534ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
36 eleq1 2825 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑧) = 𝑦 → ((𝐹𝑧) ∈ 𝑥𝑦𝑥))
3736biimparc 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥 ∧ (𝐹𝑧) = 𝑦) → (𝐹𝑧) ∈ 𝑥)
3837ad2ant2l 744 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐿𝑦𝑥) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
3938adantll 712 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
40 ffun 6671 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:𝑌𝑋 → Fun 𝐹)
41403ad2ant3 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → Fun 𝐹)
4241ad3antrrr 728 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → Fun 𝐹)
43 fdm 6677 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
4443eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝑌𝑋 → (𝑧 ∈ dom 𝐹𝑧𝑌))
4544biimpar 478 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝑌𝑋𝑧𝑌) → 𝑧 ∈ dom 𝐹)
46453ad2antl3 1187 . . . . . . . . . . . . . . . . . . . . 21 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
4746adantlr 713 . . . . . . . . . . . . . . . . . . . 20 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
4847ad2ant2r 745 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
49 fvimacnv 7003 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5042, 48, 49syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5139, 50mpbid 231 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ (𝐹𝑥))
52 n0i 4293 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝐹𝑥) → ¬ (𝐹𝑥) = ∅)
53 eqcom 2743 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = ∅ ↔ ∅ = (𝐹𝑥))
5452, 53sylnib 327 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐹𝑥) → ¬ ∅ = (𝐹𝑥))
5551, 54syl 17 . . . . . . . . . . . . . . . 16 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ¬ ∅ = (𝐹𝑥))
5655rexlimdvaa 3153 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∃𝑧𝑌 (𝐹𝑧) = 𝑦 → ¬ ∅ = (𝐹𝑥)))
5735, 56sylbid 239 . . . . . . . . . . . . . 14 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (𝐹𝑥)))
5857con2d 134 . . . . . . . . . . . . 13 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹))
5958expr 457 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑦𝑥 → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
6059com23 86 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (∅ = (𝐹𝑥) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
6160impr 455 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
6261alrimiv 1930 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
63 imnan 400 . . . . . . . . . . . 12 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦𝑥𝑦 ∈ ran 𝐹))
64 elin 3926 . . . . . . . . . . . 12 (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦𝑥𝑦 ∈ ran 𝐹))
6563, 64xchbinxr 334 . . . . . . . . . . 11 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
6665albii 1821 . . . . . . . . . 10 (∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
67 eq0 4303 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
68 eqcom 2743 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
6966, 67, 683bitr2i 298 . . . . . . . . 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 23205 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7571, 72, 73, 74syl3anc 1371 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7670, 75eqeltrd 2838 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∅ ∈ 𝐿)
7776rexlimdvaa 3153 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑥𝐿 ∅ = (𝐹𝑥) → ∅ ∈ 𝐿))
7830, 77biimtrid 241 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ∅ ∈ 𝐿))
7927, 78mtod 197 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
80 df-nel 3050 . . . 4 (∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
8179, 80sylibr 233 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)))
8219elrnmpt 5911 . . . . . . . . 9 (𝑟 ∈ V → (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥)))
8382elv 3451 . . . . . . . 8 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥))
84 imaeq2 6009 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝐹𝑥) = (𝐹𝑢))
8584eqeq2d 2747 . . . . . . . . 9 (𝑥 = 𝑢 → (𝑟 = (𝐹𝑥) ↔ 𝑟 = (𝐹𝑢)))
8685cbvrexvw 3226 . . . . . . . 8 (∃𝑥𝐿 𝑟 = (𝐹𝑥) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
8783, 86bitri 274 . . . . . . 7 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
8819elrnmpt 5911 . . . . . . . . 9 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
8988elv 3451 . . . . . . . 8 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
90 imaeq2 6009 . . . . . . . . . 10 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
9190eqeq2d 2747 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑠 = (𝐹𝑥) ↔ 𝑠 = (𝐹𝑣)))
9291cbvrexvw 3226 . . . . . . . 8 (∃𝑥𝐿 𝑠 = (𝐹𝑥) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9389, 92bitri 274 . . . . . . 7 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9487, 93anbi12i 627 . . . . . 6 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
95 reeanv 3217 . . . . . 6 (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
9694, 95bitr4i 277 . . . . 5 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))
97 filin 23205 . . . . . . . . . . . . . 14 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢𝐿𝑣𝐿) → (𝑢𝑣) ∈ 𝐿)
98973expb 1120 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
9998adantlr 713 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
100 eqidd 2737 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣)))
101 imaeq2 6009 . . . . . . . . . . . . 13 (𝑥 = (𝑢𝑣) → (𝐹𝑥) = (𝐹 “ (𝑢𝑣)))
102101rspceeqv 3595 . . . . . . . . . . . 12 (((𝑢𝑣) ∈ 𝐿 ∧ (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
10399, 100, 102syl2anc 584 . . . . . . . . . . 11 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
1041033adantl1 1166 . . . . . . . . . 10 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
105104ad2ant2r 745 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
106 simpll1 1212 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑌𝐴)
107 cnvimass 6033 . . . . . . . . . . . . . 14 (𝐹 “ (𝑢𝑣)) ⊆ dom 𝐹
108107, 43sseqtrid 3996 . . . . . . . . . . . . 13 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
1091083ad2ant3 1135 . . . . . . . . . . . 12 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
110109ad2antrr 724 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
111106, 110ssexd 5281 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ V)
11219elrnmpt 5911 . . . . . . . . . 10 ((𝐹 “ (𝑢𝑣)) ∈ V → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
113111, 112syl 17 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
114105, 113mpbird 256 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
115 simprrl 779 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑟 = (𝐹𝑢))
116 simprrr 780 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑠 = (𝐹𝑣))
117115, 116ineq12d 4173 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = ((𝐹𝑢) ∩ (𝐹𝑣)))
118 funcnvcnv 6568 . . . . . . . . . . . . 13 (Fun 𝐹 → Fun 𝐹)
119 imain 6586 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
12040, 118, 1193syl 18 . . . . . . . . . . . 12 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
1211203ad2ant3 1135 . . . . . . . . . . 11 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
122121ad2antrr 724 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
123117, 122eqtr4d 2779 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = (𝐹 “ (𝑢𝑣)))
124 eqimss2 4001 . . . . . . . . 9 ((𝑟𝑠) = (𝐹 “ (𝑢𝑣)) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
125123, 124syl 17 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
126 sseq1 3969 . . . . . . . . 9 (𝑡 = (𝐹 “ (𝑢𝑣)) → (𝑡 ⊆ (𝑟𝑠) ↔ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)))
127126rspcev 3581 . . . . . . . 8 (((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
128114, 125, 127syl2anc 584 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
129128exp32 421 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑢𝐿𝑣𝐿) → ((𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))))
130129rexlimdvv 3204 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
13196, 130biimtrid 241 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
132131ralrimivv 3195 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
13324, 81, 1323jca 1128 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
134 isfbas2 23186 . . 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 396  w3a 1087  wal 1539   = wceq 1541  wcel 2106  wne 2943  wnel 3049  wral 3064  wrex 3073  Vcvv 3445  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  cmpt 5188  ccnv 5632  dom cdm 5633  ran crn 5634  cima 5636  Fun wfun 6490   Fn wfn 6491  wf 6492  cfv 6496  fBascfbas 20784  Filcfil 23196
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 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-fbas 20793  df-fil 23197
This theorem is referenced by:  rnelfm  23304  fmfnfm  23309
  Copyright terms: Public domain W3C validator