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

Theorem fopwdom 6340
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 4706 . . . . . 6 (𝐹𝑎) ⊆ ran 𝐹
2 dfdm4 4554 . . . . . . 7 dom 𝐹 = ran 𝐹
3 fof 5133 . . . . . . . 8 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
4 fdm 5077 . . . . . . . 8 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
53, 4syl 14 . . . . . . 7 (𝐹:𝐴onto𝐵 → dom 𝐹 = 𝐴)
62, 5syl5eqr 2102 . . . . . 6 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐴)
71, 6syl5sseq 3020 . . . . 5 (𝐹:𝐴onto𝐵 → (𝐹𝑎) ⊆ 𝐴)
87adantl 266 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝐹𝑎) ⊆ 𝐴)
9 cnvexg 4882 . . . . . 6 (𝐹 ∈ V → 𝐹 ∈ V)
109adantr 265 . . . . 5 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐹 ∈ V)
11 imaexg 4707 . . . . 5 (𝐹 ∈ V → (𝐹𝑎) ∈ V)
12 elpwg 3394 . . . . 5 ((𝐹𝑎) ∈ V → ((𝐹𝑎) ∈ 𝒫 𝐴 ↔ (𝐹𝑎) ⊆ 𝐴))
1310, 11, 123syl 17 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → ((𝐹𝑎) ∈ 𝒫 𝐴 ↔ (𝐹𝑎) ⊆ 𝐴))
148, 13mpbird 160 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝐹𝑎) ∈ 𝒫 𝐴)
1514a1d 22 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝑎 ∈ 𝒫 𝐵 → (𝐹𝑎) ∈ 𝒫 𝐴))
16 imaeq2 4691 . . . . . . 7 ((𝐹𝑎) = (𝐹𝑏) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
1716adantl 266 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
18 simpllr 494 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝐹:𝐴onto𝐵)
19 simplrl 495 . . . . . . . 8 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎 ∈ 𝒫 𝐵)
2019elpwid 3396 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎𝐵)
21 foimacnv 5171 . . . . . . 7 ((𝐹:𝐴onto𝐵𝑎𝐵) → (𝐹 “ (𝐹𝑎)) = 𝑎)
2218, 20, 21syl2anc 397 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = 𝑎)
23 simplrr 496 . . . . . . . 8 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏 ∈ 𝒫 𝐵)
2423elpwid 3396 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏𝐵)
25 foimacnv 5171 . . . . . . 7 ((𝐹:𝐴onto𝐵𝑏𝐵) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2618, 24, 25syl2anc 397 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2717, 22, 263eqtr3d 2096 . . . . 5 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎 = 𝑏)
2827ex 112 . . . 4 (((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
29 imaeq2 4691 . . . 4 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
3028, 29impbid1 134 . . 3 (((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏))
3130ex 112 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → ((𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏)))
32 rnexg 4624 . . . . 5 (𝐹 ∈ V → ran 𝐹 ∈ V)
33 forn 5136 . . . . . 6 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
3433eleq1d 2122 . . . . 5 (𝐹:𝐴onto𝐵 → (ran 𝐹 ∈ V ↔ 𝐵 ∈ V))
3532, 34syl5ibcom 148 . . . 4 (𝐹 ∈ V → (𝐹:𝐴onto𝐵𝐵 ∈ V))
3635imp 119 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐵 ∈ V)
37 pwexg 3960 . . 3 (𝐵 ∈ V → 𝒫 𝐵 ∈ V)
3836, 37syl 14 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ∈ V)
39 dmfex 5106 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴𝐵) → 𝐴 ∈ V)
403, 39sylan2 274 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐴 ∈ V)
41 pwexg 3960 . . 3 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
4240, 41syl 14 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐴 ∈ V)
4315, 31, 38, 42dom3d 6284 1 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102   = wceq 1259  wcel 1409  Vcvv 2574  wss 2944  𝒫 cpw 3386   class class class wbr 3791  ccnv 4371  dom cdm 4372  ran crn 4373  cima 4375  wf 4925  ontowfo 4927  cdom 6250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-un 4197
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-opab 3846  df-mpt 3847  df-id 4057  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-fv 4937  df-dom 6253
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator