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

Theorem f1imass 6996
Description: Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.)
Assertion
Ref Expression
f1imass ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) ⊆ (𝐹𝐷) ↔ 𝐶𝐷))

Proof of Theorem f1imass
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 simplrl 776 . . . . . . 7 (((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) → 𝐶𝐴)
21sseld 3942 . . . . . 6 (((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) → (𝑎𝐶𝑎𝐴))
3 simplr 768 . . . . . . . . 9 ((((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) ∧ 𝑎𝐴) → (𝐹𝐶) ⊆ (𝐹𝐷))
43sseld 3942 . . . . . . . 8 ((((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) ∧ 𝑎𝐴) → ((𝐹𝑎) ∈ (𝐹𝐶) → (𝐹𝑎) ∈ (𝐹𝐷)))
5 simplll 774 . . . . . . . . 9 ((((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) ∧ 𝑎𝐴) → 𝐹:𝐴1-1𝐵)
6 simpr 488 . . . . . . . . 9 ((((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) ∧ 𝑎𝐴) → 𝑎𝐴)
7 simp1rl 1235 . . . . . . . . . 10 (((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷) ∧ 𝑎𝐴) → 𝐶𝐴)
873expa 1115 . . . . . . . . 9 ((((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) ∧ 𝑎𝐴) → 𝐶𝐴)
9 f1elima 6995 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝑎𝐴𝐶𝐴) → ((𝐹𝑎) ∈ (𝐹𝐶) ↔ 𝑎𝐶))
105, 6, 8, 9syl3anc 1368 . . . . . . . 8 ((((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) ∧ 𝑎𝐴) → ((𝐹𝑎) ∈ (𝐹𝐶) ↔ 𝑎𝐶))
11 simp1rr 1236 . . . . . . . . . 10 (((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷) ∧ 𝑎𝐴) → 𝐷𝐴)
12113expa 1115 . . . . . . . . 9 ((((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) ∧ 𝑎𝐴) → 𝐷𝐴)
13 f1elima 6995 . . . . . . . . 9 ((𝐹:𝐴1-1𝐵𝑎𝐴𝐷𝐴) → ((𝐹𝑎) ∈ (𝐹𝐷) ↔ 𝑎𝐷))
145, 6, 12, 13syl3anc 1368 . . . . . . . 8 ((((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) ∧ 𝑎𝐴) → ((𝐹𝑎) ∈ (𝐹𝐷) ↔ 𝑎𝐷))
154, 10, 143imtr3d 296 . . . . . . 7 ((((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) ∧ 𝑎𝐴) → (𝑎𝐶𝑎𝐷))
1615ex 416 . . . . . 6 (((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) → (𝑎𝐴 → (𝑎𝐶𝑎𝐷)))
172, 16syld 47 . . . . 5 (((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) → (𝑎𝐶 → (𝑎𝐶𝑎𝐷)))
1817pm2.43d 53 . . . 4 (((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) → (𝑎𝐶𝑎𝐷))
1918ssrdv 3949 . . 3 (((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) ∧ (𝐹𝐶) ⊆ (𝐹𝐷)) → 𝐶𝐷)
2019ex 416 . 2 ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) ⊆ (𝐹𝐷) → 𝐶𝐷))
21 imass2 5938 . 2 (𝐶𝐷 → (𝐹𝐶) ⊆ (𝐹𝐷))
2220, 21impbid1 228 1 ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) ⊆ (𝐹𝐷) ↔ 𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wcel 2115  wss 3910  cima 5531  1-1wf1 6325  cfv 6328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fv 6336
This theorem is referenced by:  f1imaeq  6997  f1imapss  6998  enfin2i  9720  tsmsf1o  22728
  Copyright terms: Public domain W3C validator