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

Theorem rnelfmlem 23676
Description: Lemma for rnelfm 23677. (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 1189 . . . . . 6 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ π‘Œ ∈ 𝐴)
2 cnvimass 6079 . . . . . . 7 (◑𝐹 β€œ π‘₯) βŠ† dom 𝐹
3 simpl3 1191 . . . . . . 7 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ 𝐹:π‘ŒβŸΆπ‘‹)
42, 3fssdm 6736 . . . . . 6 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ (◑𝐹 β€œ π‘₯) βŠ† π‘Œ)
51, 4sselpwd 5325 . . . . 5 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ (◑𝐹 β€œ π‘₯) ∈ 𝒫 π‘Œ)
65adantr 479 . . . 4 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ π‘₯ ∈ 𝐿) β†’ (◑𝐹 β€œ π‘₯) ∈ 𝒫 π‘Œ)
76fmpttd 7115 . . 3 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)):πΏβŸΆπ’« π‘Œ)
87frnd 6724 . 2 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) βŠ† 𝒫 π‘Œ)
9 filtop 23579 . . . . . . . 8 (𝐿 ∈ (Filβ€˜π‘‹) β†’ 𝑋 ∈ 𝐿)
1093ad2ant2 1132 . . . . . . 7 ((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) β†’ 𝑋 ∈ 𝐿)
1110adantr 479 . . . . . 6 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ 𝑋 ∈ 𝐿)
12 fimacnv 6738 . . . . . . . . 9 (𝐹:π‘ŒβŸΆπ‘‹ β†’ (◑𝐹 β€œ 𝑋) = π‘Œ)
1312eqcomd 2736 . . . . . . . 8 (𝐹:π‘ŒβŸΆπ‘‹ β†’ π‘Œ = (◑𝐹 β€œ 𝑋))
14133ad2ant3 1133 . . . . . . 7 ((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) β†’ π‘Œ = (◑𝐹 β€œ 𝑋))
1514adantr 479 . . . . . 6 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ π‘Œ = (◑𝐹 β€œ 𝑋))
16 imaeq2 6054 . . . . . . 7 (π‘₯ = 𝑋 β†’ (◑𝐹 β€œ π‘₯) = (◑𝐹 β€œ 𝑋))
1716rspceeqv 3632 . . . . . 6 ((𝑋 ∈ 𝐿 ∧ π‘Œ = (◑𝐹 β€œ 𝑋)) β†’ βˆƒπ‘₯ ∈ 𝐿 π‘Œ = (◑𝐹 β€œ π‘₯))
1811, 15, 17syl2anc 582 . . . . 5 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ βˆƒπ‘₯ ∈ 𝐿 π‘Œ = (◑𝐹 β€œ π‘₯))
19 eqid 2730 . . . . . . . 8 (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) = (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))
2019elrnmpt 5954 . . . . . . 7 (π‘Œ ∈ 𝐴 β†’ (π‘Œ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 π‘Œ = (◑𝐹 β€œ π‘₯)))
21203ad2ant1 1131 . . . . . 6 ((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) β†’ (π‘Œ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 π‘Œ = (◑𝐹 β€œ π‘₯)))
2221adantr 479 . . . . 5 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ (π‘Œ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 π‘Œ = (◑𝐹 β€œ π‘₯)))
2318, 22mpbird 256 . . . 4 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ π‘Œ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))
2423ne0d 4334 . . 3 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) β‰  βˆ…)
25 0nelfil 23573 . . . . . . 7 (𝐿 ∈ (Filβ€˜π‘‹) β†’ Β¬ βˆ… ∈ 𝐿)
26253ad2ant2 1132 . . . . . 6 ((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) β†’ Β¬ βˆ… ∈ 𝐿)
2726adantr 479 . . . . 5 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ Β¬ βˆ… ∈ 𝐿)
28 0ex 5306 . . . . . . 7 βˆ… ∈ V
2919elrnmpt 5954 . . . . . . 7 (βˆ… ∈ V β†’ (βˆ… ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 βˆ… = (◑𝐹 β€œ π‘₯)))
3028, 29ax-mp 5 . . . . . 6 (βˆ… ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 βˆ… = (◑𝐹 β€œ π‘₯))
31 ffn 6716 . . . . . . . . . . . . . . . . . 18 (𝐹:π‘ŒβŸΆπ‘‹ β†’ 𝐹 Fn π‘Œ)
32 fvelrnb 6951 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn π‘Œ β†’ (𝑦 ∈ ran 𝐹 ↔ βˆƒπ‘§ ∈ π‘Œ (πΉβ€˜π‘§) = 𝑦))
3331, 32syl 17 . . . . . . . . . . . . . . . . 17 (𝐹:π‘ŒβŸΆπ‘‹ β†’ (𝑦 ∈ ran 𝐹 ↔ βˆƒπ‘§ ∈ π‘Œ (πΉβ€˜π‘§) = 𝑦))
34333ad2ant3 1133 . . . . . . . . . . . . . . . 16 ((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) β†’ (𝑦 ∈ ran 𝐹 ↔ βˆƒπ‘§ ∈ π‘Œ (πΉβ€˜π‘§) = 𝑦))
3534ad2antrr 722 . . . . . . . . . . . . . . 15 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) β†’ (𝑦 ∈ ran 𝐹 ↔ βˆƒπ‘§ ∈ π‘Œ (πΉβ€˜π‘§) = 𝑦))
36 eleq1 2819 . . . . . . . . . . . . . . . . . . . . 21 ((πΉβ€˜π‘§) = 𝑦 β†’ ((πΉβ€˜π‘§) ∈ π‘₯ ↔ 𝑦 ∈ π‘₯))
3736biimparc 478 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ π‘₯ ∧ (πΉβ€˜π‘§) = 𝑦) β†’ (πΉβ€˜π‘§) ∈ π‘₯)
3837ad2ant2l 742 . . . . . . . . . . . . . . . . . . 19 (((π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ π‘Œ ∧ (πΉβ€˜π‘§) = 𝑦)) β†’ (πΉβ€˜π‘§) ∈ π‘₯)
3938adantll 710 . . . . . . . . . . . . . . . . . 18 (((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) ∧ (𝑧 ∈ π‘Œ ∧ (πΉβ€˜π‘§) = 𝑦)) β†’ (πΉβ€˜π‘§) ∈ π‘₯)
40 ffun 6719 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:π‘ŒβŸΆπ‘‹ β†’ Fun 𝐹)
41403ad2ant3 1133 . . . . . . . . . . . . . . . . . . . 20 ((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) β†’ Fun 𝐹)
4241ad3antrrr 726 . . . . . . . . . . . . . . . . . . 19 (((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) ∧ (𝑧 ∈ π‘Œ ∧ (πΉβ€˜π‘§) = 𝑦)) β†’ Fun 𝐹)
43 fdm 6725 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:π‘ŒβŸΆπ‘‹ β†’ dom 𝐹 = π‘Œ)
4443eleq2d 2817 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:π‘ŒβŸΆπ‘‹ β†’ (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ π‘Œ))
4544biimpar 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:π‘ŒβŸΆπ‘‹ ∧ 𝑧 ∈ π‘Œ) β†’ 𝑧 ∈ dom 𝐹)
46453ad2antl3 1185 . . . . . . . . . . . . . . . . . . . . 21 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ 𝑧 ∈ π‘Œ) β†’ 𝑧 ∈ dom 𝐹)
4746adantlr 711 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑧 ∈ π‘Œ) β†’ 𝑧 ∈ dom 𝐹)
4847ad2ant2r 743 . . . . . . . . . . . . . . . . . . 19 (((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) ∧ (𝑧 ∈ π‘Œ ∧ (πΉβ€˜π‘§) = 𝑦)) β†’ 𝑧 ∈ dom 𝐹)
49 fvimacnv 7053 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹) β†’ ((πΉβ€˜π‘§) ∈ π‘₯ ↔ 𝑧 ∈ (◑𝐹 β€œ π‘₯)))
5042, 48, 49syl2anc 582 . . . . . . . . . . . . . . . . . 18 (((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) ∧ (𝑧 ∈ π‘Œ ∧ (πΉβ€˜π‘§) = 𝑦)) β†’ ((πΉβ€˜π‘§) ∈ π‘₯ ↔ 𝑧 ∈ (◑𝐹 β€œ π‘₯)))
5139, 50mpbid 231 . . . . . . . . . . . . . . . . 17 (((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) ∧ (𝑧 ∈ π‘Œ ∧ (πΉβ€˜π‘§) = 𝑦)) β†’ 𝑧 ∈ (◑𝐹 β€œ π‘₯))
52 n0i 4332 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (◑𝐹 β€œ π‘₯) β†’ Β¬ (◑𝐹 β€œ π‘₯) = βˆ…)
53 eqcom 2737 . . . . . . . . . . . . . . . . . 18 ((◑𝐹 β€œ π‘₯) = βˆ… ↔ βˆ… = (◑𝐹 β€œ π‘₯))
5452, 53sylnib 327 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (◑𝐹 β€œ π‘₯) β†’ Β¬ βˆ… = (◑𝐹 β€œ π‘₯))
5551, 54syl 17 . . . . . . . . . . . . . . . 16 (((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) ∧ (𝑧 ∈ π‘Œ ∧ (πΉβ€˜π‘§) = 𝑦)) β†’ Β¬ βˆ… = (◑𝐹 β€œ π‘₯))
5655rexlimdvaa 3154 . . . . . . . . . . . . . . 15 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) β†’ (βˆƒπ‘§ ∈ π‘Œ (πΉβ€˜π‘§) = 𝑦 β†’ Β¬ βˆ… = (◑𝐹 β€œ π‘₯)))
5735, 56sylbid 239 . . . . . . . . . . . . . 14 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) β†’ (𝑦 ∈ ran 𝐹 β†’ Β¬ βˆ… = (◑𝐹 β€œ π‘₯)))
5857con2d 134 . . . . . . . . . . . . 13 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ 𝑦 ∈ π‘₯)) β†’ (βˆ… = (◑𝐹 β€œ π‘₯) β†’ Β¬ 𝑦 ∈ ran 𝐹))
5958expr 455 . . . . . . . . . . . 12 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ π‘₯ ∈ 𝐿) β†’ (𝑦 ∈ π‘₯ β†’ (βˆ… = (◑𝐹 β€œ π‘₯) β†’ Β¬ 𝑦 ∈ ran 𝐹)))
6059com23 86 . . . . . . . . . . 11 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ π‘₯ ∈ 𝐿) β†’ (βˆ… = (◑𝐹 β€œ π‘₯) β†’ (𝑦 ∈ π‘₯ β†’ Β¬ 𝑦 ∈ ran 𝐹)))
6160impr 453 . . . . . . . . . 10 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ βˆ… = (◑𝐹 β€œ π‘₯))) β†’ (𝑦 ∈ π‘₯ β†’ Β¬ 𝑦 ∈ ran 𝐹))
6261alrimiv 1928 . . . . . . . . 9 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ βˆ… = (◑𝐹 β€œ π‘₯))) β†’ βˆ€π‘¦(𝑦 ∈ π‘₯ β†’ Β¬ 𝑦 ∈ ran 𝐹))
63 imnan 398 . . . . . . . . . . . 12 ((𝑦 ∈ π‘₯ β†’ Β¬ 𝑦 ∈ ran 𝐹) ↔ Β¬ (𝑦 ∈ π‘₯ ∧ 𝑦 ∈ ran 𝐹))
64 elin 3963 . . . . . . . . . . . 12 (𝑦 ∈ (π‘₯ ∩ ran 𝐹) ↔ (𝑦 ∈ π‘₯ ∧ 𝑦 ∈ ran 𝐹))
6563, 64xchbinxr 334 . . . . . . . . . . 11 ((𝑦 ∈ π‘₯ β†’ Β¬ 𝑦 ∈ ran 𝐹) ↔ Β¬ 𝑦 ∈ (π‘₯ ∩ ran 𝐹))
6665albii 1819 . . . . . . . . . 10 (βˆ€π‘¦(𝑦 ∈ π‘₯ β†’ Β¬ 𝑦 ∈ ran 𝐹) ↔ βˆ€π‘¦ Β¬ 𝑦 ∈ (π‘₯ ∩ ran 𝐹))
67 eq0 4342 . . . . . . . . . 10 ((π‘₯ ∩ ran 𝐹) = βˆ… ↔ βˆ€π‘¦ Β¬ 𝑦 ∈ (π‘₯ ∩ ran 𝐹))
68 eqcom 2737 . . . . . . . . . 10 ((π‘₯ ∩ ran 𝐹) = βˆ… ↔ βˆ… = (π‘₯ ∩ ran 𝐹))
6966, 67, 683bitr2i 298 . . . . . . . . 9 (βˆ€π‘¦(𝑦 ∈ π‘₯ β†’ Β¬ 𝑦 ∈ ran 𝐹) ↔ βˆ… = (π‘₯ ∩ ran 𝐹))
7062, 69sylib 217 . . . . . . . 8 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ βˆ… = (◑𝐹 β€œ π‘₯))) β†’ βˆ… = (π‘₯ ∩ ran 𝐹))
71 simpll2 1211 . . . . . . . . 9 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ βˆ… = (◑𝐹 β€œ π‘₯))) β†’ 𝐿 ∈ (Filβ€˜π‘‹))
72 simprl 767 . . . . . . . . 9 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ βˆ… = (◑𝐹 β€œ π‘₯))) β†’ π‘₯ ∈ 𝐿)
73 simplr 765 . . . . . . . . 9 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ βˆ… = (◑𝐹 β€œ π‘₯))) β†’ ran 𝐹 ∈ 𝐿)
74 filin 23578 . . . . . . . . 9 ((𝐿 ∈ (Filβ€˜π‘‹) ∧ π‘₯ ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) β†’ (π‘₯ ∩ ran 𝐹) ∈ 𝐿)
7571, 72, 73, 74syl3anc 1369 . . . . . . . 8 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ βˆ… = (◑𝐹 β€œ π‘₯))) β†’ (π‘₯ ∩ ran 𝐹) ∈ 𝐿)
7670, 75eqeltrd 2831 . . . . . . 7 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ (π‘₯ ∈ 𝐿 ∧ βˆ… = (◑𝐹 β€œ π‘₯))) β†’ βˆ… ∈ 𝐿)
7776rexlimdvaa 3154 . . . . . 6 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ (βˆƒπ‘₯ ∈ 𝐿 βˆ… = (◑𝐹 β€œ π‘₯) β†’ βˆ… ∈ 𝐿))
7830, 77biimtrid 241 . . . . 5 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ (βˆ… ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) β†’ βˆ… ∈ 𝐿))
7927, 78mtod 197 . . . 4 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ Β¬ βˆ… ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))
80 df-nel 3045 . . . 4 (βˆ… βˆ‰ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ Β¬ βˆ… ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))
8179, 80sylibr 233 . . 3 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ βˆ… βˆ‰ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))
8219elrnmpt 5954 . . . . . . . . 9 (π‘Ÿ ∈ V β†’ (π‘Ÿ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 π‘Ÿ = (◑𝐹 β€œ π‘₯)))
8382elv 3478 . . . . . . . 8 (π‘Ÿ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 π‘Ÿ = (◑𝐹 β€œ π‘₯))
84 imaeq2 6054 . . . . . . . . . 10 (π‘₯ = 𝑒 β†’ (◑𝐹 β€œ π‘₯) = (◑𝐹 β€œ 𝑒))
8584eqeq2d 2741 . . . . . . . . 9 (π‘₯ = 𝑒 β†’ (π‘Ÿ = (◑𝐹 β€œ π‘₯) ↔ π‘Ÿ = (◑𝐹 β€œ 𝑒)))
8685cbvrexvw 3233 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐿 π‘Ÿ = (◑𝐹 β€œ π‘₯) ↔ βˆƒπ‘’ ∈ 𝐿 π‘Ÿ = (◑𝐹 β€œ 𝑒))
8783, 86bitri 274 . . . . . . 7 (π‘Ÿ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘’ ∈ 𝐿 π‘Ÿ = (◑𝐹 β€œ 𝑒))
8819elrnmpt 5954 . . . . . . . . 9 (𝑠 ∈ V β†’ (𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑠 = (◑𝐹 β€œ π‘₯)))
8988elv 3478 . . . . . . . 8 (𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 𝑠 = (◑𝐹 β€œ π‘₯))
90 imaeq2 6054 . . . . . . . . . 10 (π‘₯ = 𝑣 β†’ (◑𝐹 β€œ π‘₯) = (◑𝐹 β€œ 𝑣))
9190eqeq2d 2741 . . . . . . . . 9 (π‘₯ = 𝑣 β†’ (𝑠 = (◑𝐹 β€œ π‘₯) ↔ 𝑠 = (◑𝐹 β€œ 𝑣)))
9291cbvrexvw 3233 . . . . . . . 8 (βˆƒπ‘₯ ∈ 𝐿 𝑠 = (◑𝐹 β€œ π‘₯) ↔ βˆƒπ‘£ ∈ 𝐿 𝑠 = (◑𝐹 β€œ 𝑣))
9389, 92bitri 274 . . . . . . 7 (𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘£ ∈ 𝐿 𝑠 = (◑𝐹 β€œ 𝑣))
9487, 93anbi12i 625 . . . . . 6 ((π‘Ÿ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∧ 𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ (βˆƒπ‘’ ∈ 𝐿 π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ βˆƒπ‘£ ∈ 𝐿 𝑠 = (◑𝐹 β€œ 𝑣)))
95 reeanv 3224 . . . . . 6 (βˆƒπ‘’ ∈ 𝐿 βˆƒπ‘£ ∈ 𝐿 (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)) ↔ (βˆƒπ‘’ ∈ 𝐿 π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ βˆƒπ‘£ ∈ 𝐿 𝑠 = (◑𝐹 β€œ 𝑣)))
9694, 95bitr4i 277 . . . . 5 ((π‘Ÿ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∧ 𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) ↔ βˆƒπ‘’ ∈ 𝐿 βˆƒπ‘£ ∈ 𝐿 (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))
97 filin 23578 . . . . . . . . . . . . . 14 ((𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) β†’ (𝑒 ∩ 𝑣) ∈ 𝐿)
98973expb 1118 . . . . . . . . . . . . 13 ((𝐿 ∈ (Filβ€˜π‘‹) ∧ (𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) β†’ (𝑒 ∩ 𝑣) ∈ 𝐿)
9998adantlr 711 . . . . . . . . . . . 12 (((𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ (𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) β†’ (𝑒 ∩ 𝑣) ∈ 𝐿)
100 eqidd 2731 . . . . . . . . . . . 12 (((𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ (𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = (◑𝐹 β€œ (𝑒 ∩ 𝑣)))
101 imaeq2 6054 . . . . . . . . . . . . 13 (π‘₯ = (𝑒 ∩ 𝑣) β†’ (◑𝐹 β€œ π‘₯) = (◑𝐹 β€œ (𝑒 ∩ 𝑣)))
102101rspceeqv 3632 . . . . . . . . . . . 12 (((𝑒 ∩ 𝑣) ∈ 𝐿 ∧ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = (◑𝐹 β€œ (𝑒 ∩ 𝑣))) β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = (◑𝐹 β€œ π‘₯))
10399, 100, 102syl2anc 582 . . . . . . . . . . 11 (((𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ (𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = (◑𝐹 β€œ π‘₯))
1041033adantl1 1164 . . . . . . . . . 10 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ (𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = (◑𝐹 β€œ π‘₯))
105104ad2ant2r 743 . . . . . . . . 9 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = (◑𝐹 β€œ π‘₯))
106 simpll1 1210 . . . . . . . . . . 11 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ π‘Œ ∈ 𝐴)
107 cnvimass 6079 . . . . . . . . . . . . . 14 (◑𝐹 β€œ (𝑒 ∩ 𝑣)) βŠ† dom 𝐹
108107, 43sseqtrid 4033 . . . . . . . . . . . . 13 (𝐹:π‘ŒβŸΆπ‘‹ β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) βŠ† π‘Œ)
1091083ad2ant3 1133 . . . . . . . . . . . 12 ((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) βŠ† π‘Œ)
110109ad2antrr 722 . . . . . . . . . . 11 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) βŠ† π‘Œ)
111106, 110ssexd 5323 . . . . . . . . . 10 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) ∈ V)
11219elrnmpt 5954 . . . . . . . . . 10 ((◑𝐹 β€œ (𝑒 ∩ 𝑣)) ∈ V β†’ ((◑𝐹 β€œ (𝑒 ∩ 𝑣)) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = (◑𝐹 β€œ π‘₯)))
113111, 112syl 17 . . . . . . . . 9 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ ((◑𝐹 β€œ (𝑒 ∩ 𝑣)) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘₯ ∈ 𝐿 (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = (◑𝐹 β€œ π‘₯)))
114105, 113mpbird 256 . . . . . . . 8 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)))
115 simprrl 777 . . . . . . . . . . 11 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ π‘Ÿ = (◑𝐹 β€œ 𝑒))
116 simprrr 778 . . . . . . . . . . 11 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ 𝑠 = (◑𝐹 β€œ 𝑣))
117115, 116ineq12d 4212 . . . . . . . . . 10 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ (π‘Ÿ ∩ 𝑠) = ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ 𝑣)))
118 funcnvcnv 6614 . . . . . . . . . . . . 13 (Fun 𝐹 β†’ Fun ◑◑𝐹)
119 imain 6632 . . . . . . . . . . . . 13 (Fun ◑◑𝐹 β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ 𝑣)))
12040, 118, 1193syl 18 . . . . . . . . . . . 12 (𝐹:π‘ŒβŸΆπ‘‹ β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ 𝑣)))
1211203ad2ant3 1133 . . . . . . . . . . 11 ((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ 𝑣)))
122121ad2antrr 722 . . . . . . . . . 10 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) = ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ 𝑣)))
123117, 122eqtr4d 2773 . . . . . . . . 9 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ (π‘Ÿ ∩ 𝑠) = (◑𝐹 β€œ (𝑒 ∩ 𝑣)))
124 eqimss2 4040 . . . . . . . . 9 ((π‘Ÿ ∩ 𝑠) = (◑𝐹 β€œ (𝑒 ∩ 𝑣)) β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) βŠ† (π‘Ÿ ∩ 𝑠))
125123, 124syl 17 . . . . . . . 8 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) βŠ† (π‘Ÿ ∩ 𝑠))
126 sseq1 4006 . . . . . . . . 9 (𝑑 = (◑𝐹 β€œ (𝑒 ∩ 𝑣)) β†’ (𝑑 βŠ† (π‘Ÿ ∩ 𝑠) ↔ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) βŠ† (π‘Ÿ ∩ 𝑠)))
127126rspcev 3611 . . . . . . . 8 (((◑𝐹 β€œ (𝑒 ∩ 𝑣)) ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∧ (◑𝐹 β€œ (𝑒 ∩ 𝑣)) βŠ† (π‘Ÿ ∩ 𝑠)) β†’ βˆƒπ‘‘ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))𝑑 βŠ† (π‘Ÿ ∩ 𝑠))
128114, 125, 127syl2anc 582 . . . . . . 7 ((((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)))) β†’ βˆƒπ‘‘ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))𝑑 βŠ† (π‘Ÿ ∩ 𝑠))
129128exp32 419 . . . . . 6 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ ((𝑒 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) β†’ ((π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)) β†’ βˆƒπ‘‘ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))𝑑 βŠ† (π‘Ÿ ∩ 𝑠))))
130129rexlimdvv 3208 . . . . 5 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ (βˆƒπ‘’ ∈ 𝐿 βˆƒπ‘£ ∈ 𝐿 (π‘Ÿ = (◑𝐹 β€œ 𝑒) ∧ 𝑠 = (◑𝐹 β€œ 𝑣)) β†’ βˆƒπ‘‘ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))𝑑 βŠ† (π‘Ÿ ∩ 𝑠)))
13196, 130biimtrid 241 . . . 4 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ ((π‘Ÿ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∧ 𝑠 ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))) β†’ βˆƒπ‘‘ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))𝑑 βŠ† (π‘Ÿ ∩ 𝑠)))
132131ralrimivv 3196 . . 3 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ βˆ€π‘Ÿ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))βˆ€π‘  ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))βˆƒπ‘‘ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))𝑑 βŠ† (π‘Ÿ ∩ 𝑠))
13324, 81, 1323jca 1126 . 2 (((π‘Œ ∈ 𝐴 ∧ 𝐿 ∈ (Filβ€˜π‘‹) ∧ 𝐹:π‘ŒβŸΆπ‘‹) ∧ ran 𝐹 ∈ 𝐿) β†’ (ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) β‰  βˆ… ∧ βˆ… βˆ‰ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯)) ∧ βˆ€π‘Ÿ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))βˆ€π‘  ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))βˆƒπ‘‘ ∈ ran (π‘₯ ∈ 𝐿 ↦ (◑𝐹 β€œ π‘₯))𝑑 βŠ† (π‘Ÿ ∩ 𝑠)))
134 isfbas2 23559 . . 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 205   ∧ wa 394   ∧ w3a 1085  βˆ€wal 1537   = wceq 1539   ∈ wcel 2104   β‰  wne 2938   βˆ‰ wnel 3044  βˆ€wral 3059  βˆƒwrex 3068  Vcvv 3472   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601   ↦ cmpt 5230  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β€œ cima 5678  Fun wfun 6536   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  fBascfbas 21132  Filcfil 23569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-fbas 21141  df-fil 23570
This theorem is referenced by:  rnelfm  23677  fmfnfm  23682
  Copyright terms: Public domain W3C validator