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

Theorem rnelfmlem 22035
Description: Lemma for rnelfm 22036. (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 cnvimass 5667 . . . . . . 7 (𝐹𝑥) ⊆ dom 𝐹
2 simpl3 1246 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐹:𝑌𝑋)
31, 2fssdm 6239 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ⊆ 𝑌)
4 simpl1 1242 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌𝐴)
5 elpw2g 4985 . . . . . . 7 (𝑌𝐴 → ((𝐹𝑥) ∈ 𝒫 𝑌 ↔ (𝐹𝑥) ⊆ 𝑌))
64, 5syl 17 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝐹𝑥) ∈ 𝒫 𝑌 ↔ (𝐹𝑥) ⊆ 𝑌))
73, 6mpbird 248 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
87adantr 472 . . . 4 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
98fmpttd 6575 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑥𝐿 ↦ (𝐹𝑥)):𝐿⟶𝒫 𝑌)
109frnd 6230 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
11 filtop 21938 . . . . . . . 8 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
12113ad2ant2 1164 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑋𝐿)
1312adantr 472 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑋𝐿)
14 fimacnv 6537 . . . . . . . . 9 (𝐹:𝑌𝑋 → (𝐹𝑋) = 𝑌)
1514eqcomd 2771 . . . . . . . 8 (𝐹:𝑌𝑋𝑌 = (𝐹𝑋))
16153ad2ant3 1165 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑌 = (𝐹𝑋))
1716adantr 472 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 = (𝐹𝑋))
18 imaeq2 5644 . . . . . . 7 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
1918rspceeqv 3479 . . . . . 6 ((𝑋𝐿𝑌 = (𝐹𝑋)) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
2013, 17, 19syl2anc 579 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
21 eqid 2765 . . . . . . . 8 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
2221elrnmpt 5541 . . . . . . 7 (𝑌𝐴 → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
23223ad2ant1 1163 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2423adantr 472 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2520, 24mpbird 248 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
2625ne0d 4086 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅)
27 0nelfil 21932 . . . . . . 7 (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
28273ad2ant2 1164 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → ¬ ∅ ∈ 𝐿)
2928adantr 472 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ 𝐿)
30 0ex 4950 . . . . . . 7 ∅ ∈ V
3121elrnmpt 5541 . . . . . . 7 (∅ ∈ V → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥)))
3230, 31ax-mp 5 . . . . . 6 (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥))
33 ffn 6223 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
34 fvelrnb 6432 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3533, 34syl 17 . . . . . . . . . . . . . . . . 17 (𝐹:𝑌𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
36353ad2ant3 1165 . . . . . . . . . . . . . . . 16 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3736ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
38 eleq1 2832 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑧) = 𝑦 → ((𝐹𝑧) ∈ 𝑥𝑦𝑥))
3938biimparc 471 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥 ∧ (𝐹𝑧) = 𝑦) → (𝐹𝑧) ∈ 𝑥)
4039ad2ant2l 752 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐿𝑦𝑥) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
4140adantll 705 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
42 ffun 6226 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:𝑌𝑋 → Fun 𝐹)
43423ad2ant3 1165 . . . . . . . . . . . . . . . . . . . 20 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → Fun 𝐹)
4443ad3antrrr 721 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → Fun 𝐹)
45 fdm 6231 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
4645eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝑌𝑋 → (𝑧 ∈ dom 𝐹𝑧𝑌))
4746biimpar 469 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝑌𝑋𝑧𝑌) → 𝑧 ∈ dom 𝐹)
48473ad2antl3 1238 . . . . . . . . . . . . . . . . . . . . 21 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
4948adantlr 706 . . . . . . . . . . . . . . . . . . . 20 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
5049ad2ant2r 753 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
51 fvimacnv 6522 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5244, 50, 51syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5341, 52mpbid 223 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ (𝐹𝑥))
54 n0i 4084 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝐹𝑥) → ¬ (𝐹𝑥) = ∅)
55 eqcom 2772 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = ∅ ↔ ∅ = (𝐹𝑥))
5654, 55sylnib 319 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐹𝑥) → ¬ ∅ = (𝐹𝑥))
5753, 56syl 17 . . . . . . . . . . . . . . . 16 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ¬ ∅ = (𝐹𝑥))
5857rexlimdvaa 3179 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∃𝑧𝑌 (𝐹𝑧) = 𝑦 → ¬ ∅ = (𝐹𝑥)))
5937, 58sylbid 231 . . . . . . . . . . . . . 14 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (𝐹𝑥)))
6059con2d 131 . . . . . . . . . . . . 13 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹))
6160expr 448 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑦𝑥 → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
6261com23 86 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (∅ = (𝐹𝑥) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
6362impr 446 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
6463alrimiv 2022 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
65 imnan 388 . . . . . . . . . . . 12 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦𝑥𝑦 ∈ ran 𝐹))
66 elin 3958 . . . . . . . . . . . 12 (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦𝑥𝑦 ∈ ran 𝐹))
6765, 66xchbinxr 326 . . . . . . . . . . 11 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
6867albii 1914 . . . . . . . . . 10 (∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
69 eq0 4093 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
70 eqcom 2772 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
7168, 69, 703bitr2i 290 . . . . . . . . 9 (∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∅ = (𝑥 ∩ ran 𝐹))
7264, 71sylib 209 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∅ = (𝑥 ∩ ran 𝐹))
73 simpll2 1271 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → 𝐿 ∈ (Fil‘𝑋))
74 simprl 787 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → 𝑥𝐿)
75 simplr 785 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ran 𝐹𝐿)
76 filin 21937 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7773, 74, 75, 76syl3anc 1490 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7872, 77eqeltrd 2844 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∅ ∈ 𝐿)
7978rexlimdvaa 3179 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑥𝐿 ∅ = (𝐹𝑥) → ∅ ∈ 𝐿))
8032, 79syl5bi 233 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ∅ ∈ 𝐿))
8129, 80mtod 189 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
82 df-nel 3041 . . . 4 (∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
8381, 82sylibr 225 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)))
84 vex 3353 . . . . . . . . 9 𝑟 ∈ V
8521elrnmpt 5541 . . . . . . . . 9 (𝑟 ∈ V → (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥)))
8684, 85ax-mp 5 . . . . . . . 8 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥))
87 imaeq2 5644 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝐹𝑥) = (𝐹𝑢))
8887eqeq2d 2775 . . . . . . . . 9 (𝑥 = 𝑢 → (𝑟 = (𝐹𝑥) ↔ 𝑟 = (𝐹𝑢)))
8988cbvrexv 3320 . . . . . . . 8 (∃𝑥𝐿 𝑟 = (𝐹𝑥) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
9086, 89bitri 266 . . . . . . 7 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
91 vex 3353 . . . . . . . . 9 𝑠 ∈ V
9221elrnmpt 5541 . . . . . . . . 9 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
9391, 92ax-mp 5 . . . . . . . 8 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
94 imaeq2 5644 . . . . . . . . . 10 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
9594eqeq2d 2775 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑠 = (𝐹𝑥) ↔ 𝑠 = (𝐹𝑣)))
9695cbvrexv 3320 . . . . . . . 8 (∃𝑥𝐿 𝑠 = (𝐹𝑥) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9793, 96bitri 266 . . . . . . 7 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9890, 97anbi12i 620 . . . . . 6 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
99 reeanv 3254 . . . . . 6 (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
10098, 99bitr4i 269 . . . . 5 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))
101 filin 21937 . . . . . . . . . . . . . 14 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢𝐿𝑣𝐿) → (𝑢𝑣) ∈ 𝐿)
1021013expb 1149 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
103102adantlr 706 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
104 eqidd 2766 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣)))
105 imaeq2 5644 . . . . . . . . . . . . 13 (𝑥 = (𝑢𝑣) → (𝐹𝑥) = (𝐹 “ (𝑢𝑣)))
106105rspceeqv 3479 . . . . . . . . . . . 12 (((𝑢𝑣) ∈ 𝐿 ∧ (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
107103, 104, 106syl2anc 579 . . . . . . . . . . 11 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
1081073adantl1 1207 . . . . . . . . . 10 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
109108ad2ant2r 753 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
110 simpll1 1269 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑌𝐴)
111 cnvimass 5667 . . . . . . . . . . . . . 14 (𝐹 “ (𝑢𝑣)) ⊆ dom 𝐹
112111, 45syl5sseq 3813 . . . . . . . . . . . . 13 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
1131123ad2ant3 1165 . . . . . . . . . . . 12 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
114113ad2antrr 717 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
115110, 114ssexd 4966 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ V)
11621elrnmpt 5541 . . . . . . . . . 10 ((𝐹 “ (𝑢𝑣)) ∈ V → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
117115, 116syl 17 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
118109, 117mpbird 248 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
119 simprrl 799 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑟 = (𝐹𝑢))
120 simprrr 800 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑠 = (𝐹𝑣))
121119, 120ineq12d 3977 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = ((𝐹𝑢) ∩ (𝐹𝑣)))
122 funcnvcnv 6134 . . . . . . . . . . . . 13 (Fun 𝐹 → Fun 𝐹)
123 imain 6152 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
12442, 122, 1233syl 18 . . . . . . . . . . . 12 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
1251243ad2ant3 1165 . . . . . . . . . . 11 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
126125ad2antrr 717 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
127121, 126eqtr4d 2802 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = (𝐹 “ (𝑢𝑣)))
128 eqimss2 3818 . . . . . . . . 9 ((𝑟𝑠) = (𝐹 “ (𝑢𝑣)) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
129127, 128syl 17 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
130 sseq1 3786 . . . . . . . . 9 (𝑡 = (𝐹 “ (𝑢𝑣)) → (𝑡 ⊆ (𝑟𝑠) ↔ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)))
131130rspcev 3461 . . . . . . . 8 (((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
132118, 129, 131syl2anc 579 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
133132exp32 411 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑢𝐿𝑣𝐿) → ((𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))))
134133rexlimdvv 3184 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
135100, 134syl5bi 233 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
136135ralrimivv 3117 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
13726, 83, 1363jca 1158 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
138 isfbas2 21918 . . 3 (𝑌𝐴 → (ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))))
1394, 138syl 17 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))))
14010, 137, 139mpbir2and 704 1 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107  wal 1650   = wceq 1652  wcel 2155  wne 2937  wnel 3040  wral 3055  wrex 3056  Vcvv 3350  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315  cmpt 4888  ccnv 5276  dom cdm 5277  ran crn 5278  cima 5280  Fun wfun 6062   Fn wfn 6063  wf 6064  cfv 6068  fBascfbas 20007  Filcfil 21928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-fv 6076  df-fbas 20016  df-fil 21929
This theorem is referenced by:  rnelfm  22036  fmfnfm  22041
  Copyright terms: Public domain W3C validator