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

Theorem fbasrn 21981
Description: Given a filter on a domain, produce a filter on the range. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
Hypothesis
Ref Expression
fbasrn.c 𝐶 = ran (𝑥𝐵 ↦ (𝐹𝑥))
Assertion
Ref Expression
fbasrn ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → 𝐶 ∈ (fBas‘𝑌))
Distinct variable groups:   𝑥,𝐵   𝑥,𝐹   𝑥,𝑉   𝑥,𝑋   𝑥,𝑌
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem fbasrn
Dummy variables 𝑠 𝑟 𝑢 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fbasrn.c . . 3 𝐶 = ran (𝑥𝐵 ↦ (𝐹𝑥))
2 simpl2 1244 . . . . . . 7 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝐵) → 𝐹:𝑋𝑌)
3 imassrn 5661 . . . . . . . 8 (𝐹𝑥) ⊆ ran 𝐹
4 frn 6231 . . . . . . . 8 (𝐹:𝑋𝑌 → ran 𝐹𝑌)
53, 4syl5ss 3774 . . . . . . 7 (𝐹:𝑋𝑌 → (𝐹𝑥) ⊆ 𝑌)
62, 5syl 17 . . . . . 6 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝐵) → (𝐹𝑥) ⊆ 𝑌)
7 simpl3 1246 . . . . . . 7 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝐵) → 𝑌𝑉)
8 elpw2g 4987 . . . . . . 7 (𝑌𝑉 → ((𝐹𝑥) ∈ 𝒫 𝑌 ↔ (𝐹𝑥) ⊆ 𝑌))
97, 8syl 17 . . . . . 6 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝐵) → ((𝐹𝑥) ∈ 𝒫 𝑌 ↔ (𝐹𝑥) ⊆ 𝑌))
106, 9mpbird 248 . . . . 5 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝐵) → (𝐹𝑥) ∈ 𝒫 𝑌)
1110fmpttd 6579 . . . 4 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → (𝑥𝐵 ↦ (𝐹𝑥)):𝐵⟶𝒫 𝑌)
1211frnd 6232 . . 3 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ran (𝑥𝐵 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
131, 12syl5eqss 3811 . 2 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → 𝐶 ⊆ 𝒫 𝑌)
141a1i 11 . . . 4 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → 𝐶 = ran (𝑥𝐵 ↦ (𝐹𝑥)))
15 ffun 6228 . . . . . . . 8 (𝐹:𝑋𝑌 → Fun 𝐹)
16153ad2ant2 1164 . . . . . . 7 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → Fun 𝐹)
17 funimaexg 6155 . . . . . . . 8 ((Fun 𝐹𝑥𝐵) → (𝐹𝑥) ∈ V)
1817ralrimiva 3113 . . . . . . 7 (Fun 𝐹 → ∀𝑥𝐵 (𝐹𝑥) ∈ V)
19 dmmptg 5820 . . . . . . 7 (∀𝑥𝐵 (𝐹𝑥) ∈ V → dom (𝑥𝐵 ↦ (𝐹𝑥)) = 𝐵)
2016, 18, 193syl 18 . . . . . 6 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → dom (𝑥𝐵 ↦ (𝐹𝑥)) = 𝐵)
21 fbasne0 21927 . . . . . . 7 (𝐵 ∈ (fBas‘𝑋) → 𝐵 ≠ ∅)
22213ad2ant1 1163 . . . . . 6 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → 𝐵 ≠ ∅)
2320, 22eqnetrd 3004 . . . . 5 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → dom (𝑥𝐵 ↦ (𝐹𝑥)) ≠ ∅)
24 dm0rn0 5512 . . . . . 6 (dom (𝑥𝐵 ↦ (𝐹𝑥)) = ∅ ↔ ran (𝑥𝐵 ↦ (𝐹𝑥)) = ∅)
2524necon3bii 2989 . . . . 5 (dom (𝑥𝐵 ↦ (𝐹𝑥)) ≠ ∅ ↔ ran (𝑥𝐵 ↦ (𝐹𝑥)) ≠ ∅)
2623, 25sylib 209 . . . 4 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ran (𝑥𝐵 ↦ (𝐹𝑥)) ≠ ∅)
2714, 26eqnetrd 3004 . . 3 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → 𝐶 ≠ ∅)
28 fbelss 21930 . . . . . . . . 9 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝑥𝐵) → 𝑥𝑋)
2928ex 401 . . . . . . . 8 (𝐵 ∈ (fBas‘𝑋) → (𝑥𝐵𝑥𝑋))
30293ad2ant1 1163 . . . . . . 7 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → (𝑥𝐵𝑥𝑋))
31 0nelfb 21928 . . . . . . . . . 10 (𝐵 ∈ (fBas‘𝑋) → ¬ ∅ ∈ 𝐵)
32 eleq1 2832 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑥𝐵 ↔ ∅ ∈ 𝐵))
3332notbid 309 . . . . . . . . . 10 (𝑥 = ∅ → (¬ 𝑥𝐵 ↔ ¬ ∅ ∈ 𝐵))
3431, 33syl5ibrcom 238 . . . . . . . . 9 (𝐵 ∈ (fBas‘𝑋) → (𝑥 = ∅ → ¬ 𝑥𝐵))
3534con2d 131 . . . . . . . 8 (𝐵 ∈ (fBas‘𝑋) → (𝑥𝐵 → ¬ 𝑥 = ∅))
36353ad2ant1 1163 . . . . . . 7 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → (𝑥𝐵 → ¬ 𝑥 = ∅))
3730, 36jcad 508 . . . . . 6 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → (𝑥𝐵 → (𝑥𝑋 ∧ ¬ 𝑥 = ∅)))
38 fdm 6233 . . . . . . . . . . . . . . 15 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
39383ad2ant2 1164 . . . . . . . . . . . . . 14 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → dom 𝐹 = 𝑋)
4039sseq2d 3795 . . . . . . . . . . . . 13 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → (𝑥 ⊆ dom 𝐹𝑥𝑋))
4140biimpar 469 . . . . . . . . . . . 12 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝑋) → 𝑥 ⊆ dom 𝐹)
42 sseqin2 3981 . . . . . . . . . . . 12 (𝑥 ⊆ dom 𝐹 ↔ (dom 𝐹𝑥) = 𝑥)
4341, 42sylib 209 . . . . . . . . . . 11 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝑋) → (dom 𝐹𝑥) = 𝑥)
4443eqeq1d 2767 . . . . . . . . . 10 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝑋) → ((dom 𝐹𝑥) = ∅ ↔ 𝑥 = ∅))
4544biimpd 220 . . . . . . . . 9 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝑋) → ((dom 𝐹𝑥) = ∅ → 𝑥 = ∅))
4645con3d 149 . . . . . . . 8 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ 𝑥𝑋) → (¬ 𝑥 = ∅ → ¬ (dom 𝐹𝑥) = ∅))
4746expimpd 445 . . . . . . 7 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ((𝑥𝑋 ∧ ¬ 𝑥 = ∅) → ¬ (dom 𝐹𝑥) = ∅))
48 eqcom 2772 . . . . . . . . 9 (∅ = (𝐹𝑥) ↔ (𝐹𝑥) = ∅)
49 imadisj 5668 . . . . . . . . 9 ((𝐹𝑥) = ∅ ↔ (dom 𝐹𝑥) = ∅)
5048, 49bitri 266 . . . . . . . 8 (∅ = (𝐹𝑥) ↔ (dom 𝐹𝑥) = ∅)
5150notbii 311 . . . . . . 7 (¬ ∅ = (𝐹𝑥) ↔ ¬ (dom 𝐹𝑥) = ∅)
5247, 51syl6ibr 243 . . . . . 6 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ((𝑥𝑋 ∧ ¬ 𝑥 = ∅) → ¬ ∅ = (𝐹𝑥)))
5337, 52syld 47 . . . . 5 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → (𝑥𝐵 → ¬ ∅ = (𝐹𝑥)))
5453ralrimiv 3112 . . . 4 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ∀𝑥𝐵 ¬ ∅ = (𝐹𝑥))
551eleq2i 2836 . . . . . . 7 (∅ ∈ 𝐶 ↔ ∅ ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)))
56 0ex 4952 . . . . . . . 8 ∅ ∈ V
57 eqid 2765 . . . . . . . . 9 (𝑥𝐵 ↦ (𝐹𝑥)) = (𝑥𝐵 ↦ (𝐹𝑥))
5857elrnmpt 5543 . . . . . . . 8 (∅ ∈ V → (∅ ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐵 ∅ = (𝐹𝑥)))
5956, 58ax-mp 5 . . . . . . 7 (∅ ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐵 ∅ = (𝐹𝑥))
6055, 59bitri 266 . . . . . 6 (∅ ∈ 𝐶 ↔ ∃𝑥𝐵 ∅ = (𝐹𝑥))
6160notbii 311 . . . . 5 (¬ ∅ ∈ 𝐶 ↔ ¬ ∃𝑥𝐵 ∅ = (𝐹𝑥))
62 df-nel 3041 . . . . 5 (∅ ∉ 𝐶 ↔ ¬ ∅ ∈ 𝐶)
63 ralnex 3139 . . . . 5 (∀𝑥𝐵 ¬ ∅ = (𝐹𝑥) ↔ ¬ ∃𝑥𝐵 ∅ = (𝐹𝑥))
6461, 62, 633bitr4i 294 . . . 4 (∅ ∉ 𝐶 ↔ ∀𝑥𝐵 ¬ ∅ = (𝐹𝑥))
6554, 64sylibr 225 . . 3 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ∅ ∉ 𝐶)
661eleq2i 2836 . . . . . . . 8 (𝑟𝐶𝑟 ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)))
67 vex 3353 . . . . . . . . 9 𝑟 ∈ V
68 imaeq2 5646 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝐹𝑥) = (𝐹𝑢))
6968cbvmptv 4911 . . . . . . . . . 10 (𝑥𝐵 ↦ (𝐹𝑥)) = (𝑢𝐵 ↦ (𝐹𝑢))
7069elrnmpt 5543 . . . . . . . . 9 (𝑟 ∈ V → (𝑟 ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)) ↔ ∃𝑢𝐵 𝑟 = (𝐹𝑢)))
7167, 70ax-mp 5 . . . . . . . 8 (𝑟 ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)) ↔ ∃𝑢𝐵 𝑟 = (𝐹𝑢))
7266, 71bitri 266 . . . . . . 7 (𝑟𝐶 ↔ ∃𝑢𝐵 𝑟 = (𝐹𝑢))
731eleq2i 2836 . . . . . . . 8 (𝑠𝐶𝑠 ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)))
74 vex 3353 . . . . . . . . 9 𝑠 ∈ V
75 imaeq2 5646 . . . . . . . . . . 11 (𝑥 = 𝑣 → (𝐹𝑥) = (𝐹𝑣))
7675cbvmptv 4911 . . . . . . . . . 10 (𝑥𝐵 ↦ (𝐹𝑥)) = (𝑣𝐵 ↦ (𝐹𝑣))
7776elrnmpt 5543 . . . . . . . . 9 (𝑠 ∈ V → (𝑠 ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)) ↔ ∃𝑣𝐵 𝑠 = (𝐹𝑣)))
7874, 77ax-mp 5 . . . . . . . 8 (𝑠 ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)) ↔ ∃𝑣𝐵 𝑠 = (𝐹𝑣))
7973, 78bitri 266 . . . . . . 7 (𝑠𝐶 ↔ ∃𝑣𝐵 𝑠 = (𝐹𝑣))
8072, 79anbi12i 620 . . . . . 6 ((𝑟𝐶𝑠𝐶) ↔ (∃𝑢𝐵 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐵 𝑠 = (𝐹𝑣)))
81 reeanv 3254 . . . . . 6 (∃𝑢𝐵𝑣𝐵 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) ↔ (∃𝑢𝐵 𝑟 = (𝐹𝑢) ∧ ∃𝑣𝐵 𝑠 = (𝐹𝑣)))
8280, 81bitr4i 269 . . . . 5 ((𝑟𝐶𝑠𝐶) ↔ ∃𝑢𝐵𝑣𝐵 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))
83 fbasssin 21933 . . . . . . . . . . 11 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝑢𝐵𝑣𝐵) → ∃𝑤𝐵 𝑤 ⊆ (𝑢𝑣))
84833expb 1149 . . . . . . . . . 10 ((𝐵 ∈ (fBas‘𝑋) ∧ (𝑢𝐵𝑣𝐵)) → ∃𝑤𝐵 𝑤 ⊆ (𝑢𝑣))
85843ad2antl1 1236 . . . . . . . . 9 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ (𝑢𝐵𝑣𝐵)) → ∃𝑤𝐵 𝑤 ⊆ (𝑢𝑣))
8685adantrr 708 . . . . . . . 8 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ ((𝑢𝐵𝑣𝐵) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑤𝐵 𝑤 ⊆ (𝑢𝑣))
87 eqid 2765 . . . . . . . . . . . . 13 (𝐹𝑤) = (𝐹𝑤)
88 imaeq2 5646 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
8988rspceeqv 3480 . . . . . . . . . . . . 13 ((𝑤𝐵 ∧ (𝐹𝑤) = (𝐹𝑤)) → ∃𝑥𝐵 (𝐹𝑤) = (𝐹𝑥))
9087, 89mpan2 682 . . . . . . . . . . . 12 (𝑤𝐵 → ∃𝑥𝐵 (𝐹𝑤) = (𝐹𝑥))
9190ad2antrl 719 . . . . . . . . . . 11 ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣))) ∧ (𝑤𝐵𝑤 ⊆ (𝑢𝑣))) → ∃𝑥𝐵 (𝐹𝑤) = (𝐹𝑥))
921eleq2i 2836 . . . . . . . . . . . . 13 ((𝐹𝑤) ∈ 𝐶 ↔ (𝐹𝑤) ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)))
93 vex 3353 . . . . . . . . . . . . . . 15 𝑤 ∈ V
9493funimaex 6156 . . . . . . . . . . . . . 14 (Fun 𝐹 → (𝐹𝑤) ∈ V)
9557elrnmpt 5543 . . . . . . . . . . . . . 14 ((𝐹𝑤) ∈ V → ((𝐹𝑤) ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐵 (𝐹𝑤) = (𝐹𝑥)))
9616, 94, 953syl 18 . . . . . . . . . . . . 13 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ((𝐹𝑤) ∈ ran (𝑥𝐵 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐵 (𝐹𝑤) = (𝐹𝑥)))
9792, 96syl5bb 274 . . . . . . . . . . . 12 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ((𝐹𝑤) ∈ 𝐶 ↔ ∃𝑥𝐵 (𝐹𝑤) = (𝐹𝑥)))
9897ad2antrr 717 . . . . . . . . . . 11 ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣))) ∧ (𝑤𝐵𝑤 ⊆ (𝑢𝑣))) → ((𝐹𝑤) ∈ 𝐶 ↔ ∃𝑥𝐵 (𝐹𝑤) = (𝐹𝑥)))
9991, 98mpbird 248 . . . . . . . . . 10 ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣))) ∧ (𝑤𝐵𝑤 ⊆ (𝑢𝑣))) → (𝐹𝑤) ∈ 𝐶)
100 imass2 5685 . . . . . . . . . . . 12 (𝑤 ⊆ (𝑢𝑣) → (𝐹𝑤) ⊆ (𝐹 “ (𝑢𝑣)))
101100ad2antll 720 . . . . . . . . . . 11 ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣))) ∧ (𝑤𝐵𝑤 ⊆ (𝑢𝑣))) → (𝐹𝑤) ⊆ (𝐹 “ (𝑢𝑣)))
102 inss1 3994 . . . . . . . . . . . . . 14 (𝑢𝑣) ⊆ 𝑢
103 imass2 5685 . . . . . . . . . . . . . 14 ((𝑢𝑣) ⊆ 𝑢 → (𝐹 “ (𝑢𝑣)) ⊆ (𝐹𝑢))
104102, 103ax-mp 5 . . . . . . . . . . . . 13 (𝐹 “ (𝑢𝑣)) ⊆ (𝐹𝑢)
105 inss2 3995 . . . . . . . . . . . . . 14 (𝑢𝑣) ⊆ 𝑣
106 imass2 5685 . . . . . . . . . . . . . 14 ((𝑢𝑣) ⊆ 𝑣 → (𝐹 “ (𝑢𝑣)) ⊆ (𝐹𝑣))
107105, 106ax-mp 5 . . . . . . . . . . . . 13 (𝐹 “ (𝑢𝑣)) ⊆ (𝐹𝑣)
108104, 107ssini 3997 . . . . . . . . . . . 12 (𝐹 “ (𝑢𝑣)) ⊆ ((𝐹𝑢) ∩ (𝐹𝑣))
109 ineq12 3973 . . . . . . . . . . . . 13 ((𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → (𝑟𝑠) = ((𝐹𝑢) ∩ (𝐹𝑣)))
110109ad2antlr 718 . . . . . . . . . . . 12 ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣))) ∧ (𝑤𝐵𝑤 ⊆ (𝑢𝑣))) → (𝑟𝑠) = ((𝐹𝑢) ∩ (𝐹𝑣)))
111108, 110syl5sseqr 3816 . . . . . . . . . . 11 ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣))) ∧ (𝑤𝐵𝑤 ⊆ (𝑢𝑣))) → (𝐹 “ (𝑢𝑣)) ⊆ (𝑟𝑠))
112101, 111sstrd 3773 . . . . . . . . . 10 ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣))) ∧ (𝑤𝐵𝑤 ⊆ (𝑢𝑣))) → (𝐹𝑤) ⊆ (𝑟𝑠))
113 sseq1 3788 . . . . . . . . . . 11 (𝑧 = (𝐹𝑤) → (𝑧 ⊆ (𝑟𝑠) ↔ (𝐹𝑤) ⊆ (𝑟𝑠)))
114113rspcev 3462 . . . . . . . . . 10 (((𝐹𝑤) ∈ 𝐶 ∧ (𝐹𝑤) ⊆ (𝑟𝑠)) → ∃𝑧𝐶 𝑧 ⊆ (𝑟𝑠))
11599, 112, 114syl2anc 579 . . . . . . . . 9 ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣))) ∧ (𝑤𝐵𝑤 ⊆ (𝑢𝑣))) → ∃𝑧𝐶 𝑧 ⊆ (𝑟𝑠))
116115adantlrl 711 . . . . . . . 8 ((((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ ((𝑢𝐵𝑣𝐵) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) ∧ (𝑤𝐵𝑤 ⊆ (𝑢𝑣))) → ∃𝑧𝐶 𝑧 ⊆ (𝑟𝑠))
11786, 116rexlimddv 3182 . . . . . . 7 (((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) ∧ ((𝑢𝐵𝑣𝐵) ∧ (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)))) → ∃𝑧𝐶 𝑧 ⊆ (𝑟𝑠))
118117exp32 411 . . . . . 6 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ((𝑢𝐵𝑣𝐵) → ((𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑧𝐶 𝑧 ⊆ (𝑟𝑠))))
119118rexlimdvv 3184 . . . . 5 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → (∃𝑢𝐵𝑣𝐵 (𝑟 = (𝐹𝑢) ∧ 𝑠 = (𝐹𝑣)) → ∃𝑧𝐶 𝑧 ⊆ (𝑟𝑠)))
12082, 119syl5bi 233 . . . 4 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ((𝑟𝐶𝑠𝐶) → ∃𝑧𝐶 𝑧 ⊆ (𝑟𝑠)))
121120ralrimivv 3117 . . 3 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → ∀𝑟𝐶𝑠𝐶𝑧𝐶 𝑧 ⊆ (𝑟𝑠))
12227, 65, 1213jca 1158 . 2 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟𝐶𝑠𝐶𝑧𝐶 𝑧 ⊆ (𝑟𝑠)))
123 isfbas2 21932 . . 3 (𝑌𝑉 → (𝐶 ∈ (fBas‘𝑌) ↔ (𝐶 ⊆ 𝒫 𝑌 ∧ (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟𝐶𝑠𝐶𝑧𝐶 𝑧 ⊆ (𝑟𝑠)))))
1241233ad2ant3 1165 . 2 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → (𝐶 ∈ (fBas‘𝑌) ↔ (𝐶 ⊆ 𝒫 𝑌 ∧ (𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀𝑟𝐶𝑠𝐶𝑧𝐶 𝑧 ⊆ (𝑟𝑠)))))
12513, 122, 124mpbir2and 704 1 ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌𝑉) → 𝐶 ∈ (fBas‘𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wnel 3040  wral 3055  wrex 3056  Vcvv 3350  cin 3733  wss 3734  c0 4081  𝒫 cpw 4317  cmpt 4890  dom cdm 5279  ran crn 5280  cima 5282  Fun wfun 6064  wf 6066  cfv 6070  fBascfbas 20021
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-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064
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 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-fv 6078  df-fbas 20030
This theorem is referenced by:  fmfil  22041  fmss  22043  elfm  22044  fmucnd  22389  fmcfil  23363
  Copyright terms: Public domain W3C validator