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

Theorem rnelfmlem 22249
Description: Lemma for rnelfm 22250. (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 1184 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌𝐴)
2 cnvimass 5830 . . . . . . 7 (𝐹𝑥) ⊆ dom 𝐹
3 simpl3 1186 . . . . . . 7 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝐹:𝑌𝑋)
42, 3fssdm 6403 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ⊆ 𝑌)
51, 4sselpwd 5126 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
65adantr 481 . . . 4 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝐹𝑥) ∈ 𝒫 𝑌)
76fmpttd 6747 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑥𝐿 ↦ (𝐹𝑥)):𝐿⟶𝒫 𝑌)
87frnd 6394 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
9 filtop 22152 . . . . . . . 8 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
1093ad2ant2 1127 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑋𝐿)
1110adantr 481 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑋𝐿)
12 fimacnv 6709 . . . . . . . . 9 (𝐹:𝑌𝑋 → (𝐹𝑋) = 𝑌)
1312eqcomd 2801 . . . . . . . 8 (𝐹:𝑌𝑋𝑌 = (𝐹𝑋))
14133ad2ant3 1128 . . . . . . 7 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → 𝑌 = (𝐹𝑋))
1514adantr 481 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 = (𝐹𝑋))
16 imaeq2 5807 . . . . . . 7 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
1716rspceeqv 3577 . . . . . 6 ((𝑋𝐿𝑌 = (𝐹𝑋)) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
1811, 15, 17syl2anc 584 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∃𝑥𝐿 𝑌 = (𝐹𝑥))
19 eqid 2795 . . . . . . . 8 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
2019elrnmpt 5715 . . . . . . 7 (𝑌𝐴 → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
21203ad2ant1 1126 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2221adantr 481 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑌 = (𝐹𝑥)))
2318, 22mpbird 258 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → 𝑌 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
2423ne0d 4225 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅)
25 0nelfil 22146 . . . . . . 7 (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
26253ad2ant2 1127 . . . . . 6 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → ¬ ∅ ∈ 𝐿)
2726adantr 481 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ 𝐿)
28 0ex 5107 . . . . . . 7 ∅ ∈ V
2919elrnmpt 5715 . . . . . . 7 (∅ ∈ V → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥)))
3028, 29ax-mp 5 . . . . . 6 (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 ∅ = (𝐹𝑥))
31 ffn 6387 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
32 fvelrnb 6599 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3331, 32syl 17 . . . . . . . . . . . . . . . . 17 (𝐹:𝑌𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
34333ad2ant3 1128 . . . . . . . . . . . . . . . 16 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
3534ad2antrr 722 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧𝑌 (𝐹𝑧) = 𝑦))
36 eleq1 2870 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑧) = 𝑦 → ((𝐹𝑧) ∈ 𝑥𝑦𝑥))
3736biimparc 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥 ∧ (𝐹𝑧) = 𝑦) → (𝐹𝑧) ∈ 𝑥)
3837ad2ant2l 742 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐿𝑦𝑥) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
3938adantll 710 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → (𝐹𝑧) ∈ 𝑥)
40 ffun 6390 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:𝑌𝑋 → Fun 𝐹)
41403ad2ant3 1128 . . . . . . . . . . . . . . . . . . . 20 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → Fun 𝐹)
4241ad3antrrr 726 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → Fun 𝐹)
43 fdm 6395 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
4443eleq2d 2868 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝑌𝑋 → (𝑧 ∈ dom 𝐹𝑧𝑌))
4544biimpar 478 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝑌𝑋𝑧𝑌) → 𝑧 ∈ dom 𝐹)
46453ad2antl3 1180 . . . . . . . . . . . . . . . . . . . . 21 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
4746adantlr 711 . . . . . . . . . . . . . . . . . . . 20 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑧𝑌) → 𝑧 ∈ dom 𝐹)
4847ad2ant2r 743 . . . . . . . . . . . . . . . . . . 19 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
49 fvimacnv 6693 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹𝑧 ∈ dom 𝐹) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5042, 48, 49syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ((𝐹𝑧) ∈ 𝑥𝑧 ∈ (𝐹𝑥)))
5139, 50mpbid 233 . . . . . . . . . . . . . . . . 17 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → 𝑧 ∈ (𝐹𝑥))
52 n0i 4223 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝐹𝑥) → ¬ (𝐹𝑥) = ∅)
53 eqcom 2802 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = ∅ ↔ ∅ = (𝐹𝑥))
5452, 53sylnib 329 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐹𝑥) → ¬ ∅ = (𝐹𝑥))
5551, 54syl 17 . . . . . . . . . . . . . . . 16 (((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) ∧ (𝑧𝑌 ∧ (𝐹𝑧) = 𝑦)) → ¬ ∅ = (𝐹𝑥))
5655rexlimdvaa 3248 . . . . . . . . . . . . . . 15 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∃𝑧𝑌 (𝐹𝑧) = 𝑦 → ¬ ∅ = (𝐹𝑥)))
5735, 56sylbid 241 . . . . . . . . . . . . . 14 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (𝐹𝑥)))
5857con2d 136 . . . . . . . . . . . . 13 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿𝑦𝑥)) → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹))
5958expr 457 . . . . . . . . . . . 12 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (𝑦𝑥 → (∅ = (𝐹𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
6059com23 86 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ 𝑥𝐿) → (∅ = (𝐹𝑥) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
6160impr 455 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
6261alrimiv 1905 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹))
63 imnan 400 . . . . . . . . . . . 12 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦𝑥𝑦 ∈ ran 𝐹))
64 elin 4094 . . . . . . . . . . . 12 (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦𝑥𝑦 ∈ ran 𝐹))
6563, 64xchbinxr 336 . . . . . . . . . . 11 ((𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
6665albii 1801 . . . . . . . . . 10 (∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
67 eq0 4232 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
68 eqcom 2802 . . . . . . . . . 10 ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
6966, 67, 683bitr2i 300 . . . . . . . . 9 (∀𝑦(𝑦𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∅ = (𝑥 ∩ ran 𝐹))
7062, 69sylib 219 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∅ = (𝑥 ∩ ran 𝐹))
71 simpll2 1206 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → 𝐿 ∈ (Fil‘𝑋))
72 simprl 767 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → 𝑥𝐿)
73 simplr 765 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ran 𝐹𝐿)
74 filin 22151 . . . . . . . . 9 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥𝐿 ∧ ran 𝐹𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7571, 72, 73, 74syl3anc 1364 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
7670, 75eqeltrd 2883 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ (𝑥𝐿 ∧ ∅ = (𝐹𝑥))) → ∅ ∈ 𝐿)
7776rexlimdvaa 3248 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑥𝐿 ∅ = (𝐹𝑥) → ∅ ∈ 𝐿))
7830, 77syl5bi 243 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → ∅ ∈ 𝐿))
7927, 78mtod 199 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
80 df-nel 3091 . . . 4 (∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ¬ ∅ ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
8179, 80sylibr 235 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)))
8219elrnmpt 5715 . . . . . . . . 9 (𝑟 ∈ V → (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥)))
8382elv 3442 . . . . . . . 8 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑟 = (𝐹𝑥))
84 imaeq2 5807 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝐹𝑥) = (𝐹𝑢))
8584eqeq2d 2805 . . . . . . . . 9 (𝑥 = 𝑢 → (𝑟 = (𝐹𝑥) ↔ 𝑟 = (𝐹𝑢)))
8685cbvrexv 3404 . . . . . . . 8 (∃𝑥𝐿 𝑟 = (𝐹𝑥) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
8783, 86bitri 276 . . . . . . 7 (𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑢𝐿 𝑟 = (𝐹𝑢))
8819elrnmpt 5715 . . . . . . . . 9 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥)))
8988elv 3442 . . . . . . . 8 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑠 = (𝐹𝑥))
90 imaeq2 5807 . . . . . . . . . 10 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
9190eqeq2d 2805 . . . . . . . . 9 (𝑥 = 𝑣 → (𝑠 = (𝐹𝑥) ↔ 𝑠 = (𝐹𝑣)))
9291cbvrexv 3404 . . . . . . . 8 (∃𝑥𝐿 𝑠 = (𝐹𝑥) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9389, 92bitri 276 . . . . . . 7 (𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑣𝐿 𝑠 = (𝐹𝑣))
9487, 93anbi12i 626 . . . . . 6 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
95 reeanv 3328 . . . . . 6 (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) ↔ (∃𝑢𝐿 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐿 𝑠 = (𝐹𝑣)))
9694, 95bitr4i 279 . . . . 5 ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) ↔ ∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))
97 filin 22151 . . . . . . . . . . . . . 14 ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢𝐿𝑣𝐿) → (𝑢𝑣) ∈ 𝐿)
98973expb 1113 . . . . . . . . . . . . 13 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
9998adantlr 711 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝑢𝑣) ∈ 𝐿)
100 eqidd 2796 . . . . . . . . . . . 12 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣)))
101 imaeq2 5807 . . . . . . . . . . . . 13 (𝑥 = (𝑢𝑣) → (𝐹𝑥) = (𝐹 “ (𝑢𝑣)))
102101rspceeqv 3577 . . . . . . . . . . . 12 (((𝑢𝑣) ∈ 𝐿 ∧ (𝐹 “ (𝑢𝑣)) = (𝐹 “ (𝑢𝑣))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
10399, 100, 102syl2anc 584 . . . . . . . . . . 11 (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
1041033adantl1 1159 . . . . . . . . . 10 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ (𝑢𝐿𝑣𝐿)) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
105104ad2ant2r 743 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥))
106 simpll1 1205 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑌𝐴)
107 cnvimass 5830 . . . . . . . . . . . . . 14 (𝐹 “ (𝑢𝑣)) ⊆ dom 𝐹
108107, 43sseqtrid 3944 . . . . . . . . . . . . 13 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
1091083ad2ant3 1128 . . . . . . . . . . . 12 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
110109ad2antrr 722 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ 𝑌)
111106, 110ssexd 5124 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ V)
11219elrnmpt 5715 . . . . . . . . . 10 ((𝐹 “ (𝑢𝑣)) ∈ V → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
113111, 112syl 17 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 (𝐹 “ (𝑢𝑣)) = (𝐹𝑥)))
114105, 113mpbird 258 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)))
115 simprrl 777 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑟 = (𝐹𝑢))
116 simprrr 778 . . . . . . . . . . 11 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → 𝑠 = (𝐹𝑣))
117115, 116ineq12d 4114 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = ((𝐹𝑢) ∩ (𝐹𝑣)))
118 funcnvcnv 6296 . . . . . . . . . . . . 13 (Fun 𝐹 → Fun 𝐹)
119 imain 6314 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
12040, 118, 1193syl 18 . . . . . . . . . . . 12 (𝐹:𝑌𝑋 → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
1211203ad2ant3 1128 . . . . . . . . . . 11 ((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
122121ad2antrr 722 . . . . . . . . . 10 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) = ((𝐹𝑢) ∩ (𝐹𝑣)))
123117, 122eqtr4d 2834 . . . . . . . . 9 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝑟𝑠) = (𝐹 “ (𝑢𝑣)))
124 eqimss2 3949 . . . . . . . . 9 ((𝑟𝑠) = (𝐹 “ (𝑢𝑣)) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
125123, 124syl 17 . . . . . . . 8 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
126 sseq1 3917 . . . . . . . . 9 (𝑡 = (𝐹 “ (𝑢𝑣)) → (𝑡 ⊆ (𝑟𝑠) ↔ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)))
127126rspcev 3559 . . . . . . . 8 (((𝐹 “ (𝑢𝑣)) ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
128114, 125, 127syl2anc 584 . . . . . . 7 ((((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) ∧ ((𝑢𝐿𝑣𝐿) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
129128exp32 421 . . . . . 6 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑢𝐿𝑣𝐿) → ((𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))))
130129rexlimdvv 3256 . . . . 5 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (∃𝑢𝐿𝑣𝐿 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
13196, 130syl5bi 243 . . . 4 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ((𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ 𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) → ∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
132131ralrimivv 3157 . . 3 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠))
13324, 81, 1323jca 1121 . 2 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → (ran (𝑥𝐿 ↦ (𝐹𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∧ ∀𝑟 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∀𝑠 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))∃𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))𝑡 ⊆ (𝑟𝑠)))
134 isfbas2 22132 . . 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 709 1 (((𝑌𝐴𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1080  wal 1520   = wceq 1522  wcel 2081  wne 2984  wnel 3090  wral 3105  wrex 3106  Vcvv 3437  cin 3862  wss 3863  c0 4215  𝒫 cpw 4457  cmpt 5045  ccnv 5447  dom cdm 5448  ran crn 5449  cima 5451  Fun wfun 6224   Fn wfn 6225  wf 6226  cfv 6230  fBascfbas 20220  Filcfil 22142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-fv 6238  df-fbas 20229  df-fil 22143
This theorem is referenced by:  rnelfm  22250  fmfnfm  22255
  Copyright terms: Public domain W3C validator