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

Theorem fopwdom 6738
Description: Covering implies injection on power sets. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
fopwdom ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴)

Proof of Theorem fopwdom
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imassrn 4900 . . . . . 6 (𝐹𝑎) ⊆ ran 𝐹
2 dfdm4 4739 . . . . . . 7 dom 𝐹 = ran 𝐹
3 fof 5353 . . . . . . . 8 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
4 fdm 5286 . . . . . . . 8 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
53, 4syl 14 . . . . . . 7 (𝐹:𝐴onto𝐵 → dom 𝐹 = 𝐴)
62, 5syl5eqr 2187 . . . . . 6 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐴)
71, 6sseqtrid 3152 . . . . 5 (𝐹:𝐴onto𝐵 → (𝐹𝑎) ⊆ 𝐴)
87adantl 275 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝐹𝑎) ⊆ 𝐴)
9 cnvexg 5084 . . . . . 6 (𝐹 ∈ V → 𝐹 ∈ V)
109adantr 274 . . . . 5 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐹 ∈ V)
11 imaexg 4901 . . . . 5 (𝐹 ∈ V → (𝐹𝑎) ∈ V)
12 elpwg 3523 . . . . 5 ((𝐹𝑎) ∈ V → ((𝐹𝑎) ∈ 𝒫 𝐴 ↔ (𝐹𝑎) ⊆ 𝐴))
1310, 11, 123syl 17 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → ((𝐹𝑎) ∈ 𝒫 𝐴 ↔ (𝐹𝑎) ⊆ 𝐴))
148, 13mpbird 166 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝐹𝑎) ∈ 𝒫 𝐴)
1514a1d 22 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝑎 ∈ 𝒫 𝐵 → (𝐹𝑎) ∈ 𝒫 𝐴))
16 imaeq2 4885 . . . . . . 7 ((𝐹𝑎) = (𝐹𝑏) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
1716adantl 275 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
18 simpllr 524 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝐹:𝐴onto𝐵)
19 simplrl 525 . . . . . . . 8 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎 ∈ 𝒫 𝐵)
2019elpwid 3526 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎𝐵)
21 foimacnv 5393 . . . . . . 7 ((𝐹:𝐴onto𝐵𝑎𝐵) → (𝐹 “ (𝐹𝑎)) = 𝑎)
2218, 20, 21syl2anc 409 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = 𝑎)
23 simplrr 526 . . . . . . . 8 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏 ∈ 𝒫 𝐵)
2423elpwid 3526 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏𝐵)
25 foimacnv 5393 . . . . . . 7 ((𝐹:𝐴onto𝐵𝑏𝐵) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2618, 24, 25syl2anc 409 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2717, 22, 263eqtr3d 2181 . . . . 5 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎 = 𝑏)
2827ex 114 . . . 4 (((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
29 imaeq2 4885 . . . 4 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
3028, 29impbid1 141 . . 3 (((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏))
3130ex 114 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → ((𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏)))
32 rnexg 4812 . . . . 5 (𝐹 ∈ V → ran 𝐹 ∈ V)
33 forn 5356 . . . . . 6 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
3433eleq1d 2209 . . . . 5 (𝐹:𝐴onto𝐵 → (ran 𝐹 ∈ V ↔ 𝐵 ∈ V))
3532, 34syl5ibcom 154 . . . 4 (𝐹 ∈ V → (𝐹:𝐴onto𝐵𝐵 ∈ V))
3635imp 123 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐵 ∈ V)
37 pwexg 4112 . . 3 (𝐵 ∈ V → 𝒫 𝐵 ∈ V)
3836, 37syl 14 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ∈ V)
39 dmfex 5320 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴𝐵) → 𝐴 ∈ V)
403, 39sylan2 284 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐴 ∈ V)
41 pwexg 4112 . . 3 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
4240, 41syl 14 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐴 ∈ V)
4315, 31, 38, 42dom3d 6676 1 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1332  wcel 1481  Vcvv 2689  wss 3076  𝒫 cpw 3515   class class class wbr 3937  ccnv 4546  dom cdm 4547  ran crn 4548  cima 4550  wf 5127  ontowfo 5129  cdom 6641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-un 4363
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-opab 3998  df-mpt 3999  df-id 4223  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-fv 5139  df-dom 6644
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator