Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elrfirn Structured version   Visualization version   GIF version

Theorem elrfirn 37784
 Description: Elementhood in a set of relative finite intersections of an indexed family of sets. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Assertion
Ref Expression
elrfirn ((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 𝑦𝑣 (𝐹𝑦))))
Distinct variable groups:   𝑣,𝐴   𝑣,𝐵   𝑣,𝐹,𝑦   𝑣,𝐼   𝑣,𝑉   𝑦,𝑣
Allowed substitution hints:   𝐴(𝑦)   𝐵(𝑦)   𝐼(𝑦)   𝑉(𝑦)

Proof of Theorem elrfirn
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 frn 6193 . . 3 (𝐹:𝐼⟶𝒫 𝐵 → ran 𝐹 ⊆ 𝒫 𝐵)
2 elrfi 37783 . . 3 ((𝐵𝑉 ∧ ran 𝐹 ⊆ 𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)𝐴 = (𝐵 𝑤)))
31, 2sylan2 580 . 2 ((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)𝐴 = (𝐵 𝑤)))
4 imassrn 5618 . . . . . 6 (𝐹𝑣) ⊆ ran 𝐹
5 pwexg 4980 . . . . . . . 8 (𝐵𝑉 → 𝒫 𝐵 ∈ V)
6 ssexg 4938 . . . . . . . 8 ((ran 𝐹 ⊆ 𝒫 𝐵 ∧ 𝒫 𝐵 ∈ V) → ran 𝐹 ∈ V)
71, 5, 6syl2anr 584 . . . . . . 7 ((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) → ran 𝐹 ∈ V)
8 elpw2g 4958 . . . . . . 7 (ran 𝐹 ∈ V → ((𝐹𝑣) ∈ 𝒫 ran 𝐹 ↔ (𝐹𝑣) ⊆ ran 𝐹))
97, 8syl 17 . . . . . 6 ((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) → ((𝐹𝑣) ∈ 𝒫 ran 𝐹 ↔ (𝐹𝑣) ⊆ ran 𝐹))
104, 9mpbiri 248 . . . . 5 ((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) → (𝐹𝑣) ∈ 𝒫 ran 𝐹)
1110adantr 466 . . . 4 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐹𝑣) ∈ 𝒫 ran 𝐹)
12 ffun 6188 . . . . . 6 (𝐹:𝐼⟶𝒫 𝐵 → Fun 𝐹)
1312ad2antlr 706 . . . . 5 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → Fun 𝐹)
14 inss2 3982 . . . . . . 7 (𝒫 𝐼 ∩ Fin) ⊆ Fin
1514sseli 3748 . . . . . 6 (𝑣 ∈ (𝒫 𝐼 ∩ Fin) → 𝑣 ∈ Fin)
1615adantl 467 . . . . 5 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → 𝑣 ∈ Fin)
17 imafi 8415 . . . . 5 ((Fun 𝐹𝑣 ∈ Fin) → (𝐹𝑣) ∈ Fin)
1813, 16, 17syl2anc 573 . . . 4 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐹𝑣) ∈ Fin)
1911, 18elind 3949 . . 3 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐹𝑣) ∈ (𝒫 ran 𝐹 ∩ Fin))
20 ffn 6185 . . . . . 6 (𝐹:𝐼⟶𝒫 𝐵𝐹 Fn 𝐼)
2120ad2antlr 706 . . . . 5 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → 𝐹 Fn 𝐼)
22 inss1 3981 . . . . . . . 8 (𝒫 ran 𝐹 ∩ Fin) ⊆ 𝒫 ran 𝐹
2322sseli 3748 . . . . . . 7 (𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin) → 𝑤 ∈ 𝒫 ran 𝐹)
2423elpwid 4309 . . . . . 6 (𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin) → 𝑤 ⊆ ran 𝐹)
2524adantl 467 . . . . 5 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → 𝑤 ⊆ ran 𝐹)
26 inss2 3982 . . . . . . 7 (𝒫 ran 𝐹 ∩ Fin) ⊆ Fin
2726sseli 3748 . . . . . 6 (𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin) → 𝑤 ∈ Fin)
2827adantl 467 . . . . 5 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → 𝑤 ∈ Fin)
29 fipreima 8428 . . . . 5 ((𝐹 Fn 𝐼𝑤 ⊆ ran 𝐹𝑤 ∈ Fin) → ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)(𝐹𝑣) = 𝑤)
3021, 25, 28, 29syl3anc 1476 . . . 4 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)(𝐹𝑣) = 𝑤)
31 eqcom 2778 . . . . 5 ((𝐹𝑣) = 𝑤𝑤 = (𝐹𝑣))
3231rexbii 3189 . . . 4 (∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)(𝐹𝑣) = 𝑤 ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝑤 = (𝐹𝑣))
3330, 32sylib 208 . . 3 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)) → ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝑤 = (𝐹𝑣))
34 inteq 4614 . . . . . 6 (𝑤 = (𝐹𝑣) → 𝑤 = (𝐹𝑣))
3534ineq2d 3965 . . . . 5 (𝑤 = (𝐹𝑣) → (𝐵 𝑤) = (𝐵 (𝐹𝑣)))
3635eqeq2d 2781 . . . 4 (𝑤 = (𝐹𝑣) → (𝐴 = (𝐵 𝑤) ↔ 𝐴 = (𝐵 (𝐹𝑣))))
3736adantl 467 . . 3 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑤 = (𝐹𝑣)) → (𝐴 = (𝐵 𝑤) ↔ 𝐴 = (𝐵 (𝐹𝑣))))
3819, 33, 37rexxfrd 5009 . 2 ((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) → (∃𝑤 ∈ (𝒫 ran 𝐹 ∩ Fin)𝐴 = (𝐵 𝑤) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 (𝐹𝑣))))
3920ad2antlr 706 . . . . . . 7 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → 𝐹 Fn 𝐼)
40 inss1 3981 . . . . . . . . . 10 (𝒫 𝐼 ∩ Fin) ⊆ 𝒫 𝐼
4140sseli 3748 . . . . . . . . 9 (𝑣 ∈ (𝒫 𝐼 ∩ Fin) → 𝑣 ∈ 𝒫 𝐼)
4241elpwid 4309 . . . . . . . 8 (𝑣 ∈ (𝒫 𝐼 ∩ Fin) → 𝑣𝐼)
4342adantl 467 . . . . . . 7 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → 𝑣𝐼)
44 imaiinfv 37782 . . . . . . 7 ((𝐹 Fn 𝐼𝑣𝐼) → 𝑦𝑣 (𝐹𝑦) = (𝐹𝑣))
4539, 43, 44syl2anc 573 . . . . . 6 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → 𝑦𝑣 (𝐹𝑦) = (𝐹𝑣))
4645eqcomd 2777 . . . . 5 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐹𝑣) = 𝑦𝑣 (𝐹𝑦))
4746ineq2d 3965 . . . 4 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐵 (𝐹𝑣)) = (𝐵 𝑦𝑣 (𝐹𝑦)))
4847eqeq2d 2781 . . 3 (((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) ∧ 𝑣 ∈ (𝒫 𝐼 ∩ Fin)) → (𝐴 = (𝐵 (𝐹𝑣)) ↔ 𝐴 = (𝐵 𝑦𝑣 (𝐹𝑦))))
4948rexbidva 3197 . 2 ((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) → (∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 (𝐹𝑣)) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 𝑦𝑣 (𝐹𝑦))))
503, 38, 493bitrd 294 1 ((𝐵𝑉𝐹:𝐼⟶𝒫 𝐵) → (𝐴 ∈ (fi‘({𝐵} ∪ ran 𝐹)) ↔ ∃𝑣 ∈ (𝒫 𝐼 ∩ Fin)𝐴 = (𝐵 𝑦𝑣 (𝐹𝑦))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ∃wrex 3062  Vcvv 3351   ∪ cun 3721   ∩ cin 3722   ⊆ wss 3723  𝒫 cpw 4297  {csn 4316  ∩ cint 4611  ∩ ciin 4655  ran crn 5250   “ cima 5252  Fun wfun 6025   Fn wfn 6026  ⟶wf 6027  ‘cfv 6031  Fincfn 8109  ficfi 8472 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-en 8110  df-dom 8111  df-fin 8113  df-fi 8473 This theorem is referenced by:  elrfirn2  37785
 Copyright terms: Public domain W3C validator