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

Theorem fopwdom 6246
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 𝐹:AontoB) → 𝒫 B ≼ 𝒫 A)

Proof of Theorem fopwdom
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imassrn 4622 . . . . . 6 (𝐹𝑎) ⊆ ran 𝐹
2 dfdm4 4470 . . . . . . 7 dom 𝐹 = ran 𝐹
3 fof 5049 . . . . . . . 8 (𝐹:AontoB𝐹:AB)
4 fdm 4993 . . . . . . . 8 (𝐹:AB → dom 𝐹 = A)
53, 4syl 14 . . . . . . 7 (𝐹:AontoB → dom 𝐹 = A)
62, 5syl5eqr 2083 . . . . . 6 (𝐹:AontoB → ran 𝐹 = A)
71, 6syl5sseq 2987 . . . . 5 (𝐹:AontoB → (𝐹𝑎) ⊆ A)
87adantl 262 . . . 4 ((𝐹 V 𝐹:AontoB) → (𝐹𝑎) ⊆ A)
9 cnvexg 4798 . . . . . 6 (𝐹 V → 𝐹 V)
109adantr 261 . . . . 5 ((𝐹 V 𝐹:AontoB) → 𝐹 V)
11 imaexg 4623 . . . . 5 (𝐹 V → (𝐹𝑎) V)
12 elpwg 3359 . . . . 5 ((𝐹𝑎) V → ((𝐹𝑎) 𝒫 A ↔ (𝐹𝑎) ⊆ A))
1310, 11, 123syl 17 . . . 4 ((𝐹 V 𝐹:AontoB) → ((𝐹𝑎) 𝒫 A ↔ (𝐹𝑎) ⊆ A))
148, 13mpbird 156 . . 3 ((𝐹 V 𝐹:AontoB) → (𝐹𝑎) 𝒫 A)
1514a1d 22 . 2 ((𝐹 V 𝐹:AontoB) → (𝑎 𝒫 B → (𝐹𝑎) 𝒫 A))
16 imaeq2 4607 . . . . . . 7 ((𝐹𝑎) = (𝐹𝑏) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
1716adantl 262 . . . . . 6 ((((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = (𝐹 “ (𝐹𝑏)))
18 simpllr 486 . . . . . . 7 ((((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) (𝐹𝑎) = (𝐹𝑏)) → 𝐹:AontoB)
19 simplrl 487 . . . . . . . 8 ((((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) (𝐹𝑎) = (𝐹𝑏)) → 𝑎 𝒫 B)
2019elpwid 3361 . . . . . . 7 ((((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) (𝐹𝑎) = (𝐹𝑏)) → 𝑎B)
21 foimacnv 5087 . . . . . . 7 ((𝐹:AontoB 𝑎B) → (𝐹 “ (𝐹𝑎)) = 𝑎)
2218, 20, 21syl2anc 391 . . . . . 6 ((((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑎)) = 𝑎)
23 simplrr 488 . . . . . . . 8 ((((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) (𝐹𝑎) = (𝐹𝑏)) → 𝑏 𝒫 B)
2423elpwid 3361 . . . . . . 7 ((((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) (𝐹𝑎) = (𝐹𝑏)) → 𝑏B)
25 foimacnv 5087 . . . . . . 7 ((𝐹:AontoB 𝑏B) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2618, 24, 25syl2anc 391 . . . . . 6 ((((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) (𝐹𝑎) = (𝐹𝑏)) → (𝐹 “ (𝐹𝑏)) = 𝑏)
2717, 22, 263eqtr3d 2077 . . . . 5 ((((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) (𝐹𝑎) = (𝐹𝑏)) → 𝑎 = 𝑏)
2827ex 108 . . . 4 (((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
29 imaeq2 4607 . . . 4 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
3028, 29impbid1 130 . . 3 (((𝐹 V 𝐹:AontoB) (𝑎 𝒫 B 𝑏 𝒫 B)) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏))
3130ex 108 . 2 ((𝐹 V 𝐹:AontoB) → ((𝑎 𝒫 B 𝑏 𝒫 B) → ((𝐹𝑎) = (𝐹𝑏) ↔ 𝑎 = 𝑏)))
32 rnexg 4540 . . . . 5 (𝐹 V → ran 𝐹 V)
33 forn 5052 . . . . . 6 (𝐹:AontoB → ran 𝐹 = B)
3433eleq1d 2103 . . . . 5 (𝐹:AontoB → (ran 𝐹 V ↔ B V))
3532, 34syl5ibcom 144 . . . 4 (𝐹 V → (𝐹:AontoBB V))
3635imp 115 . . 3 ((𝐹 V 𝐹:AontoB) → B V)
37 pwexg 3924 . . 3 (B V → 𝒫 B V)
3836, 37syl 14 . 2 ((𝐹 V 𝐹:AontoB) → 𝒫 B V)
39 dmfex 5022 . . . 4 ((𝐹 V 𝐹:AB) → A V)
403, 39sylan2 270 . . 3 ((𝐹 V 𝐹:AontoB) → A V)
41 pwexg 3924 . . 3 (A V → 𝒫 A V)
4240, 41syl 14 . 2 ((𝐹 V 𝐹:AontoB) → 𝒫 A V)
4315, 31, 38, 42dom3d 6190 1 ((𝐹 V 𝐹:AontoB) → 𝒫 B ≼ 𝒫 A)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1242   wcel 1390  Vcvv 2551  wss 2911  𝒫 cpw 3351   class class class wbr 3755  ccnv 4287  dom cdm 4288  ran crn 4289  cima 4291  wf 4841  ontowfo 4843  cdom 6156
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-fv 4853  df-dom 6159
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator