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

Theorem fopwdom 6532
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 4772 . . . . . 6 (𝐹𝑎) ⊆ ran 𝐹
2 dfdm4 4616 . . . . . . 7 dom 𝐹 = ran 𝐹
3 fof 5217 . . . . . . . 8 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
4 fdm 5152 . . . . . . . 8 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
53, 4syl 14 . . . . . . 7 (𝐹:𝐴onto𝐵 → dom 𝐹 = 𝐴)
62, 5syl5eqr 2134 . . . . . 6 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐴)
71, 6syl5sseq 3072 . . . . 5 (𝐹:𝐴onto𝐵 → (𝐹𝑎) ⊆ 𝐴)
87adantl 271 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝐹𝑎) ⊆ 𝐴)
9 cnvexg 4955 . . . . . 6 (𝐹 ∈ V → 𝐹 ∈ V)
109adantr 270 . . . . 5 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐹 ∈ V)
11 imaexg 4773 . . . . 5 (𝐹 ∈ V → (𝐹𝑎) ∈ V)
12 elpwg 3433 . . . . 5 ((𝐹𝑎) ∈ V → ((𝐹𝑎) ∈ 𝒫 𝐴 ↔ (𝐹𝑎) ⊆ 𝐴))
1310, 11, 123syl 17 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → ((𝐹𝑎) ∈ 𝒫 𝐴 ↔ (𝐹𝑎) ⊆ 𝐴))
148, 13mpbird 165 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝐹𝑎) ∈ 𝒫 𝐴)
1514a1d 22 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝑎 ∈ 𝒫 𝐵 → (𝐹𝑎) ∈ 𝒫 𝐴))
16 imaeq2 4757 . . . . . . 7 ((𝐹𝑎) = (𝐹𝑏) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
1716adantl 271 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
18 simpllr 501 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝐹:𝐴onto𝐵)
19 simplrl 502 . . . . . . . 8 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎 ∈ 𝒫 𝐵)
2019elpwid 3435 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎𝐵)
21 foimacnv 5255 . . . . . . 7 ((𝐹:𝐴onto𝐵𝑎𝐵) → (𝐹 “ (𝐹𝑎)) = 𝑎)
2218, 20, 21syl2anc 403 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = 𝑎)
23 simplrr 503 . . . . . . . 8 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏 ∈ 𝒫 𝐵)
2423elpwid 3435 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏𝐵)
25 foimacnv 5255 . . . . . . 7 ((𝐹:𝐴onto𝐵𝑏𝐵) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2618, 24, 25syl2anc 403 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2717, 22, 263eqtr3d 2128 . . . . 5 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎 = 𝑏)
2827ex 113 . . . 4 (((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
29 imaeq2 4757 . . . 4 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
3028, 29impbid1 140 . . 3 (((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏))
3130ex 113 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → ((𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏)))
32 rnexg 4686 . . . . 5 (𝐹 ∈ V → ran 𝐹 ∈ V)
33 forn 5220 . . . . . 6 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
3433eleq1d 2156 . . . . 5 (𝐹:𝐴onto𝐵 → (ran 𝐹 ∈ V ↔ 𝐵 ∈ V))
3532, 34syl5ibcom 153 . . . 4 (𝐹 ∈ V → (𝐹:𝐴onto𝐵𝐵 ∈ V))
3635imp 122 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐵 ∈ V)
37 pwexg 4007 . . 3 (𝐵 ∈ V → 𝒫 𝐵 ∈ V)
3836, 37syl 14 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ∈ V)
39 dmfex 5184 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴𝐵) → 𝐴 ∈ V)
403, 39sylan2 280 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐴 ∈ V)
41 pwexg 4007 . . 3 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
4240, 41syl 14 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐴 ∈ V)
4315, 31, 38, 42dom3d 6471 1 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1289  wcel 1438  Vcvv 2619  wss 2997  𝒫 cpw 3425   class class class wbr 3837  ccnv 4427  dom cdm 4428  ran crn 4429  cima 4431  wf 4998  ontowfo 5000  cdom 6436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027  ax-un 4251
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-mpt 3893  df-id 4111  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-fv 5010  df-dom 6439
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator