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

Theorem dffi2 9252
Description: The set of finite intersections is the smallest set that contains 𝐴 and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013.)
Assertion
Ref Expression
dffi2 (𝐴𝑉 → (fi‘𝐴) = {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)})
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑦,𝑉,𝑧
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem dffi2
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 elex 3459 . 2 (𝐴𝑉𝐴 ∈ V)
2 vex 3445 . . . . . . . . . 10 𝑡 ∈ V
3 elfi 9242 . . . . . . . . . 10 ((𝑡 ∈ V ∧ 𝐴 ∈ V) → (𝑡 ∈ (fi‘𝐴) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = 𝑥))
42, 3mpan 687 . . . . . . . . 9 (𝐴 ∈ V → (𝑡 ∈ (fi‘𝐴) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = 𝑥))
54biimpd 228 . . . . . . . 8 (𝐴 ∈ V → (𝑡 ∈ (fi‘𝐴) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = 𝑥))
6 df-rex 3072 . . . . . . . . 9 (∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = 𝑥 ↔ ∃𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥))
7 fiint 9161 . . . . . . . . . . . 12 (∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧 ↔ ∀𝑥((𝑥𝑧𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝑧))
8 elinel1 4140 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴)
98elpwid 4554 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥𝐴)
1093ad2ant2 1133 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑧𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑥𝐴)
11 simp1 1135 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑧𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝐴𝑧)
1210, 11sstrd 3941 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑧𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑥𝑧)
13 eqvisset 3458 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑥 𝑥 ∈ V)
14 intex 5276 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ≠ ∅ ↔ 𝑥 ∈ V)
1513, 14sylibr 233 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑥𝑥 ≠ ∅)
16153ad2ant3 1134 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑧𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑥 ≠ ∅)
17 elinel2 4141 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin)
18173ad2ant2 1133 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑧𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑥 ∈ Fin)
1912, 16, 183jca 1127 . . . . . . . . . . . . . . . . 17 ((𝐴𝑧𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → (𝑥𝑧𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin))
20193expib 1121 . . . . . . . . . . . . . . . 16 (𝐴𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → (𝑥𝑧𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin)))
21 pm2.27 42 . . . . . . . . . . . . . . . 16 ((𝑥𝑧𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → (((𝑥𝑧𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝑧) → 𝑥𝑧))
2220, 21syl6 35 . . . . . . . . . . . . . . 15 (𝐴𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → (((𝑥𝑧𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝑧) → 𝑥𝑧)))
23 eleq1 2825 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑥 → (𝑡𝑧 𝑥𝑧))
2423biimprd 247 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑥 → ( 𝑥𝑧𝑡𝑧))
2524adantl 482 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → ( 𝑥𝑧𝑡𝑧))
2625a1i 11 . . . . . . . . . . . . . . 15 (𝐴𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → ( 𝑥𝑧𝑡𝑧)))
2722, 26syldd 72 . . . . . . . . . . . . . 14 (𝐴𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → (((𝑥𝑧𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝑧) → 𝑡𝑧)))
2827com23 86 . . . . . . . . . . . . 13 (𝐴𝑧 → (((𝑥𝑧𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝑧) → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑡𝑧)))
2928alimdv 1918 . . . . . . . . . . . 12 (𝐴𝑧 → (∀𝑥((𝑥𝑧𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝑧) → ∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑡𝑧)))
307, 29biimtrid 241 . . . . . . . . . . 11 (𝐴𝑧 → (∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧 → ∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑡𝑧)))
3130imp 407 . . . . . . . . . 10 ((𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) → ∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑡𝑧))
32 19.23v 1944 . . . . . . . . . 10 (∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑡𝑧) ↔ (∃𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑡𝑧))
3331, 32sylib 217 . . . . . . . . 9 ((𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) → (∃𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = 𝑥) → 𝑡𝑧))
346, 33biimtrid 241 . . . . . . . 8 ((𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) → (∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = 𝑥𝑡𝑧))
355, 34sylan9 508 . . . . . . 7 ((𝐴 ∈ V ∧ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)) → (𝑡 ∈ (fi‘𝐴) → 𝑡𝑧))
3635ssrdv 3937 . . . . . 6 ((𝐴 ∈ V ∧ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)) → (fi‘𝐴) ⊆ 𝑧)
3736ex 413 . . . . 5 (𝐴 ∈ V → ((𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) → (fi‘𝐴) ⊆ 𝑧))
3837alrimiv 1929 . . . 4 (𝐴 ∈ V → ∀𝑧((𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) → (fi‘𝐴) ⊆ 𝑧))
39 ssintab 4909 . . . 4 ((fi‘𝐴) ⊆ {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)} ↔ ∀𝑧((𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) → (fi‘𝐴) ⊆ 𝑧))
4038, 39sylibr 233 . . 3 (𝐴 ∈ V → (fi‘𝐴) ⊆ {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)})
41 ssfii 9248 . . . . 5 (𝐴 ∈ V → 𝐴 ⊆ (fi‘𝐴))
42 fiin 9251 . . . . . 6 ((𝑥 ∈ (fi‘𝐴) ∧ 𝑦 ∈ (fi‘𝐴)) → (𝑥𝑦) ∈ (fi‘𝐴))
4342rgen2 3191 . . . . 5 𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥𝑦) ∈ (fi‘𝐴)
44 fvex 6824 . . . . . 6 (fi‘𝐴) ∈ V
45 sseq2 3957 . . . . . . 7 (𝑧 = (fi‘𝐴) → (𝐴𝑧𝐴 ⊆ (fi‘𝐴)))
46 eleq2 2826 . . . . . . . . 9 (𝑧 = (fi‘𝐴) → ((𝑥𝑦) ∈ 𝑧 ↔ (𝑥𝑦) ∈ (fi‘𝐴)))
4746raleqbi1dv 3304 . . . . . . . 8 (𝑧 = (fi‘𝐴) → (∀𝑦𝑧 (𝑥𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ (fi‘𝐴)(𝑥𝑦) ∈ (fi‘𝐴)))
4847raleqbi1dv 3304 . . . . . . 7 (𝑧 = (fi‘𝐴) → (∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧 ↔ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥𝑦) ∈ (fi‘𝐴)))
4945, 48anbi12d 631 . . . . . 6 (𝑧 = (fi‘𝐴) → ((𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧) ↔ (𝐴 ⊆ (fi‘𝐴) ∧ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥𝑦) ∈ (fi‘𝐴))))
5044, 49elab 3619 . . . . 5 ((fi‘𝐴) ∈ {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)} ↔ (𝐴 ⊆ (fi‘𝐴) ∧ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥𝑦) ∈ (fi‘𝐴)))
5141, 43, 50sylanblrc 590 . . . 4 (𝐴 ∈ V → (fi‘𝐴) ∈ {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)})
52 intss1 4907 . . . 4 ((fi‘𝐴) ∈ {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)} → {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)} ⊆ (fi‘𝐴))
5351, 52syl 17 . . 3 (𝐴 ∈ V → {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)} ⊆ (fi‘𝐴))
5440, 53eqssd 3948 . 2 (𝐴 ∈ V → (fi‘𝐴) = {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)})
551, 54syl 17 1 (𝐴𝑉 → (fi‘𝐴) = {𝑧 ∣ (𝐴𝑧 ∧ ∀𝑥𝑧𝑦𝑧 (𝑥𝑦) ∈ 𝑧)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086  wal 1538   = wceq 1540  wex 1780  wcel 2105  {cab 2714  wne 2941  wral 3062  wrex 3071  Vcvv 3441  cin 3896  wss 3897  c0 4267  𝒫 cpw 4545   cint 4892  cfv 6465  Fincfn 8781  ficfi 9239
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-int 4893  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-om 7758  df-1o 8344  df-er 8546  df-en 8782  df-fin 8785  df-fi 9240
This theorem is referenced by:  fiss  9253  inficl  9254  dffi3  9260  fbssfi  23060
  Copyright terms: Public domain W3C validator