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

Theorem fopwdom 6310
 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 4679 . . . . . 6 (𝐹𝑎) ⊆ ran 𝐹
2 dfdm4 4527 . . . . . . 7 dom 𝐹 = ran 𝐹
3 fof 5106 . . . . . . . 8 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
4 fdm 5050 . . . . . . . 8 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
53, 4syl 14 . . . . . . 7 (𝐹:𝐴onto𝐵 → dom 𝐹 = 𝐴)
62, 5syl5eqr 2086 . . . . . 6 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐴)
71, 6syl5sseq 2993 . . . . 5 (𝐹:𝐴onto𝐵 → (𝐹𝑎) ⊆ 𝐴)
87adantl 262 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝐹𝑎) ⊆ 𝐴)
9 cnvexg 4855 . . . . . 6 (𝐹 ∈ V → 𝐹 ∈ V)
109adantr 261 . . . . 5 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐹 ∈ V)
11 imaexg 4680 . . . . 5 (𝐹 ∈ V → (𝐹𝑎) ∈ V)
12 elpwg 3367 . . . . 5 ((𝐹𝑎) ∈ V → ((𝐹𝑎) ∈ 𝒫 𝐴 ↔ (𝐹𝑎) ⊆ 𝐴))
1310, 11, 123syl 17 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → ((𝐹𝑎) ∈ 𝒫 𝐴 ↔ (𝐹𝑎) ⊆ 𝐴))
148, 13mpbird 156 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝐹𝑎) ∈ 𝒫 𝐴)
1514a1d 22 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → (𝑎 ∈ 𝒫 𝐵 → (𝐹𝑎) ∈ 𝒫 𝐴))
16 imaeq2 4664 . . . . . . 7 ((𝐹𝑎) = (𝐹𝑏) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
1716adantl 262 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
18 simpllr 486 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝐹:𝐴onto𝐵)
19 simplrl 487 . . . . . . . 8 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎 ∈ 𝒫 𝐵)
2019elpwid 3369 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎𝐵)
21 foimacnv 5144 . . . . . . 7 ((𝐹:𝐴onto𝐵𝑎𝐵) → (𝐹 “ (𝐹𝑎)) = 𝑎)
2218, 20, 21syl2anc 391 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = 𝑎)
23 simplrr 488 . . . . . . . 8 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏 ∈ 𝒫 𝐵)
2423elpwid 3369 . . . . . . 7 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏𝐵)
25 foimacnv 5144 . . . . . . 7 ((𝐹:𝐴onto𝐵𝑏𝐵) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2618, 24, 25syl2anc 391 . . . . . 6 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2717, 22, 263eqtr3d 2080 . . . . 5 ((((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎 = 𝑏)
2827ex 108 . . . 4 (((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
29 imaeq2 4664 . . . 4 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
3028, 29impbid1 130 . . 3 (((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) ∧ (𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵)) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏))
3130ex 108 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → ((𝑎 ∈ 𝒫 𝐵𝑏 ∈ 𝒫 𝐵) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏)))
32 rnexg 4597 . . . . 5 (𝐹 ∈ V → ran 𝐹 ∈ V)
33 forn 5109 . . . . . 6 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
3433eleq1d 2106 . . . . 5 (𝐹:𝐴onto𝐵 → (ran 𝐹 ∈ V ↔ 𝐵 ∈ V))
3532, 34syl5ibcom 144 . . . 4 (𝐹 ∈ V → (𝐹:𝐴onto𝐵𝐵 ∈ V))
3635imp 115 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐵 ∈ V)
37 pwexg 3933 . . 3 (𝐵 ∈ V → 𝒫 𝐵 ∈ V)
3836, 37syl 14 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ∈ V)
39 dmfex 5079 . . . 4 ((𝐹 ∈ V ∧ 𝐹:𝐴𝐵) → 𝐴 ∈ V)
403, 39sylan2 270 . . 3 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝐴 ∈ V)
41 pwexg 3933 . . 3 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
4240, 41syl 14 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐴 ∈ V)
4315, 31, 38, 42dom3d 6254 1 ((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243   ∈ wcel 1393  Vcvv 2557   ⊆ wss 2917  𝒫 cpw 3359   class class class wbr 3764  ◡ccnv 4344  dom cdm 4345  ran crn 4346   “ cima 4348  ⟶wf 4898  –onto→wfo 4900   ≼ cdom 6220 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-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944  ax-un 4170 This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-mpt 3820  df-id 4030  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-fv 4910  df-dom 6223 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator