ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imadiflem Structured version   GIF version

Theorem imadiflem 4904
Description: One direction of imadif 4905. This direction does not require Fun 𝐹. (Contributed by Jim Kingdon, 25-Dec-2018.)
Assertion
Ref Expression
imadiflem ((𝐹A) ∖ (𝐹B)) ⊆ (𝐹 “ (AB))

Proof of Theorem imadiflem
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rex 2290 . . . 4 (x A x𝐹yx(x A x𝐹y))
2 df-rex 2290 . . . . 5 (x B x𝐹yx(x B x𝐹y))
32notbii 581 . . . 4 x B x𝐹y ↔ ¬ x(x B x𝐹y))
4 alnex 1369 . . . . . . 7 (x ¬ (x B x𝐹y) ↔ ¬ x(x B x𝐹y))
5 19.29r 1494 . . . . . . 7 ((x(x A x𝐹y) x ¬ (x B x𝐹y)) → x((x A x𝐹y) ¬ (x B x𝐹y)))
64, 5sylan2br 272 . . . . . 6 ((x(x A x𝐹y) ¬ x(x B x𝐹y)) → x((x A x𝐹y) ¬ (x B x𝐹y)))
7 ax-ia1 99 . . . . . . . . 9 (((x A x𝐹y) ¬ (x B x𝐹y)) → (x A x𝐹y))
8 simplr 470 . . . . . . . . . 10 (((x A x𝐹y) ¬ (x B x𝐹y)) → x𝐹y)
9 ax-ia2 100 . . . . . . . . . . 11 (((x A x𝐹y) ¬ (x B x𝐹y)) → ¬ (x B x𝐹y))
10 ancom 253 . . . . . . . . . . . . 13 ((x B x𝐹y) ↔ (x𝐹y x B))
1110notbii 581 . . . . . . . . . . . 12 (¬ (x B x𝐹y) ↔ ¬ (x𝐹y x B))
12 imnan 611 . . . . . . . . . . . 12 ((x𝐹y → ¬ x B) ↔ ¬ (x𝐹y x B))
1311, 12bitr4i 176 . . . . . . . . . . 11 (¬ (x B x𝐹y) ↔ (x𝐹y → ¬ x B))
149, 13sylib 127 . . . . . . . . . 10 (((x A x𝐹y) ¬ (x B x𝐹y)) → (x𝐹y → ¬ x B))
158, 14mpd 13 . . . . . . . . 9 (((x A x𝐹y) ¬ (x B x𝐹y)) → ¬ x B)
167, 15, 8jca32 293 . . . . . . . 8 (((x A x𝐹y) ¬ (x B x𝐹y)) → ((x A x𝐹y) x B x𝐹y)))
17 eldif 2904 . . . . . . . . . 10 (x (AB) ↔ (x A ¬ x B))
1817anbi1i 434 . . . . . . . . 9 ((x (AB) x𝐹y) ↔ ((x A ¬ x B) x𝐹y))
19 anandir 512 . . . . . . . . 9 (((x A ¬ x B) x𝐹y) ↔ ((x A x𝐹y) x B x𝐹y)))
2018, 19bitri 173 . . . . . . . 8 ((x (AB) x𝐹y) ↔ ((x A x𝐹y) x B x𝐹y)))
2116, 20sylibr 137 . . . . . . 7 (((x A x𝐹y) ¬ (x B x𝐹y)) → (x (AB) x𝐹y))
2221eximi 1473 . . . . . 6 (x((x A x𝐹y) ¬ (x B x𝐹y)) → x(x (AB) x𝐹y))
236, 22syl 14 . . . . 5 ((x(x A x𝐹y) ¬ x(x B x𝐹y)) → x(x (AB) x𝐹y))
24 df-rex 2290 . . . . 5 (x (AB)x𝐹yx(x (AB) x𝐹y))
2523, 24sylibr 137 . . . 4 ((x(x A x𝐹y) ¬ x(x B x𝐹y)) → x (AB)x𝐹y)
261, 3, 25syl2anb 275 . . 3 ((x A x𝐹y ¬ x B x𝐹y) → x (AB)x𝐹y)
2726ss2abi 2989 . 2 {y ∣ (x A x𝐹y ¬ x B x𝐹y)} ⊆ {yx (AB)x𝐹y}
28 dfima2 4597 . . . 4 (𝐹A) = {yx A x𝐹y}
29 dfima2 4597 . . . 4 (𝐹B) = {yx B x𝐹y}
3028, 29difeq12i 3037 . . 3 ((𝐹A) ∖ (𝐹B)) = ({yx A x𝐹y} ∖ {yx B x𝐹y})
31 difab 3183 . . 3 ({yx A x𝐹y} ∖ {yx B x𝐹y}) = {y ∣ (x A x𝐹y ¬ x B x𝐹y)}
3230, 31eqtri 2042 . 2 ((𝐹A) ∖ (𝐹B)) = {y ∣ (x A x𝐹y ¬ x B x𝐹y)}
33 dfima2 4597 . 2 (𝐹 “ (AB)) = {yx (AB)x𝐹y}
3427, 32, 333sstr4i 2961 1 ((𝐹A) ∖ (𝐹B)) ⊆ (𝐹 “ (AB))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wal 1226  wex 1362   wcel 1374  {cab 2008  wrex 2285  cdif 2891  wss 2894   class class class wbr 3738  cima 4275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901  ax-pr 3918
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-rex 2290  df-rab 2293  df-v 2537  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-br 3739  df-opab 3793  df-xp 4278  df-cnv 4280  df-dm 4282  df-rn 4283  df-res 4284  df-ima 4285
This theorem is referenced by:  imadif  4905
  Copyright terms: Public domain W3C validator