MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  php3OLD Structured version   Visualization version   GIF version

Theorem php3OLD 9287
Description: Obsolete version of php3 9275 as of 26-Nov-2024. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
php3OLD ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵𝐴)

Proof of Theorem php3OLD
Dummy variables 𝑥 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 9036 . . 3 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
2 relen 9008 . . . . . . . . 9 Rel ≈
32brrelex1i 5756 . . . . . . . 8 (𝐴𝑥𝐴 ∈ V)
4 pssss 4121 . . . . . . . 8 (𝐵𝐴𝐵𝐴)
5 ssdomg 9060 . . . . . . . . 9 (𝐴 ∈ V → (𝐵𝐴𝐵𝐴))
65imp 406 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐵𝐴) → 𝐵𝐴)
73, 4, 6syl2an 595 . . . . . . 7 ((𝐴𝑥𝐵𝐴) → 𝐵𝐴)
87adantll 713 . . . . . 6 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → 𝐵𝐴)
9 bren 9013 . . . . . . . . 9 (𝐴𝑥 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝑥)
10 imass2 6132 . . . . . . . . . . . . . . . . 17 (𝐵𝐴 → (𝑓𝐵) ⊆ (𝑓𝐴))
114, 10syl 17 . . . . . . . . . . . . . . . 16 (𝐵𝐴 → (𝑓𝐵) ⊆ (𝑓𝐴))
1211adantl 481 . . . . . . . . . . . . . . 15 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊆ (𝑓𝐴))
13 pssnel 4494 . . . . . . . . . . . . . . . . 17 (𝐵𝐴 → ∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵))
14 eldif 3986 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴 ∧ ¬ 𝑦𝐵))
15 f1ofn 6863 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝐴1-1-onto𝑥𝑓 Fn 𝐴)
16 difss 4159 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴𝐵) ⊆ 𝐴
17 fnfvima 7270 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 Fn 𝐴 ∧ (𝐴𝐵) ⊆ 𝐴𝑦 ∈ (𝐴𝐵)) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵)))
18173expia 1121 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 Fn 𝐴 ∧ (𝐴𝐵) ⊆ 𝐴) → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵))))
1915, 16, 18sylancl 585 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵))))
20 dff1o3 6868 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:𝐴1-1-onto𝑥 ↔ (𝑓:𝐴onto𝑥 ∧ Fun 𝑓))
21 imadif 6662 . . . . . . . . . . . . . . . . . . . . . . . 24 (Fun 𝑓 → (𝑓 “ (𝐴𝐵)) = ((𝑓𝐴) ∖ (𝑓𝐵)))
2220, 21simplbiim 504 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝐴1-1-onto𝑥 → (𝑓 “ (𝐴𝐵)) = ((𝑓𝐴) ∖ (𝑓𝐵)))
2322eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:𝐴1-1-onto𝑥 → ((𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵)) ↔ (𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵))))
2419, 23sylibd 239 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵))))
25 n0i 4363 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵)) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
2624, 25syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2714, 26biimtrrid 243 . . . . . . . . . . . . . . . . . . 19 (𝑓:𝐴1-1-onto𝑥 → ((𝑦𝐴 ∧ ¬ 𝑦𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2827exlimdv 1932 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴1-1-onto𝑥 → (∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2928imp 406 . . . . . . . . . . . . . . . . 17 ((𝑓:𝐴1-1-onto𝑥 ∧ ∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵)) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
3013, 29sylan2 592 . . . . . . . . . . . . . . . 16 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
31 ssdif0 4389 . . . . . . . . . . . . . . . 16 ((𝑓𝐴) ⊆ (𝑓𝐵) ↔ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
3230, 31sylnibr 329 . . . . . . . . . . . . . . 15 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ¬ (𝑓𝐴) ⊆ (𝑓𝐵))
33 dfpss3 4112 . . . . . . . . . . . . . . 15 ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ ((𝑓𝐵) ⊆ (𝑓𝐴) ∧ ¬ (𝑓𝐴) ⊆ (𝑓𝐵)))
3412, 32, 33sylanbrc 582 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊊ (𝑓𝐴))
35 imadmrn 6099 . . . . . . . . . . . . . . . . 17 (𝑓 “ dom 𝑓) = ran 𝑓
36 f1odm 6866 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴1-1-onto𝑥 → dom 𝑓 = 𝐴)
3736imaeq2d 6089 . . . . . . . . . . . . . . . . 17 (𝑓:𝐴1-1-onto𝑥 → (𝑓 “ dom 𝑓) = (𝑓𝐴))
38 f1ofo 6869 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴1-1-onto𝑥𝑓:𝐴onto𝑥)
39 forn 6837 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴onto𝑥 → ran 𝑓 = 𝑥)
4038, 39syl 17 . . . . . . . . . . . . . . . . 17 (𝑓:𝐴1-1-onto𝑥 → ran 𝑓 = 𝑥)
4135, 37, 403eqtr3a 2804 . . . . . . . . . . . . . . . 16 (𝑓:𝐴1-1-onto𝑥 → (𝑓𝐴) = 𝑥)
4241psseq2d 4119 . . . . . . . . . . . . . . 15 (𝑓:𝐴1-1-onto𝑥 → ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ (𝑓𝐵) ⊊ 𝑥))
4342adantr 480 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ (𝑓𝐵) ⊊ 𝑥))
4434, 43mpbid 232 . . . . . . . . . . . . 13 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊊ 𝑥)
45 php 9273 . . . . . . . . . . . . 13 ((𝑥 ∈ ω ∧ (𝑓𝐵) ⊊ 𝑥) → ¬ 𝑥 ≈ (𝑓𝐵))
4644, 45sylan2 592 . . . . . . . . . . . 12 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → ¬ 𝑥 ≈ (𝑓𝐵))
47 f1of1 6861 . . . . . . . . . . . . . . . 16 (𝑓:𝐴1-1-onto𝑥𝑓:𝐴1-1𝑥)
48 f1ores 6876 . . . . . . . . . . . . . . . 16 ((𝑓:𝐴1-1𝑥𝐵𝐴) → (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵))
4947, 4, 48syl2an 595 . . . . . . . . . . . . . . 15 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵))
50 vex 3492 . . . . . . . . . . . . . . . . . 18 𝑓 ∈ V
5150resex 6058 . . . . . . . . . . . . . . . . 17 (𝑓𝐵) ∈ V
52 f1oeq1 6850 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑓𝐵) → (𝑦:𝐵1-1-onto→(𝑓𝐵) ↔ (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵)))
5351, 52spcev 3619 . . . . . . . . . . . . . . . 16 ((𝑓𝐵):𝐵1-1-onto→(𝑓𝐵) → ∃𝑦 𝑦:𝐵1-1-onto→(𝑓𝐵))
54 bren 9013 . . . . . . . . . . . . . . . 16 (𝐵 ≈ (𝑓𝐵) ↔ ∃𝑦 𝑦:𝐵1-1-onto→(𝑓𝐵))
5553, 54sylibr 234 . . . . . . . . . . . . . . 15 ((𝑓𝐵):𝐵1-1-onto→(𝑓𝐵) → 𝐵 ≈ (𝑓𝐵))
5649, 55syl 17 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → 𝐵 ≈ (𝑓𝐵))
57 entr 9066 . . . . . . . . . . . . . . 15 ((𝑥𝐵𝐵 ≈ (𝑓𝐵)) → 𝑥 ≈ (𝑓𝐵))
5857expcom 413 . . . . . . . . . . . . . 14 (𝐵 ≈ (𝑓𝐵) → (𝑥𝐵𝑥 ≈ (𝑓𝐵)))
5956, 58syl 17 . . . . . . . . . . . . 13 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑥𝐵𝑥 ≈ (𝑓𝐵)))
6059adantl 481 . . . . . . . . . . . 12 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → (𝑥𝐵𝑥 ≈ (𝑓𝐵)))
6146, 60mtod 198 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → ¬ 𝑥𝐵)
6261exp32 420 . . . . . . . . . 10 (𝑥 ∈ ω → (𝑓:𝐴1-1-onto𝑥 → (𝐵𝐴 → ¬ 𝑥𝐵)))
6362exlimdv 1932 . . . . . . . . 9 (𝑥 ∈ ω → (∃𝑓 𝑓:𝐴1-1-onto𝑥 → (𝐵𝐴 → ¬ 𝑥𝐵)))
649, 63biimtrid 242 . . . . . . . 8 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴 → ¬ 𝑥𝐵)))
6564imp31 417 . . . . . . 7 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → ¬ 𝑥𝐵)
66 entr 9066 . . . . . . . . . 10 ((𝐵𝐴𝐴𝑥) → 𝐵𝑥)
6766ex 412 . . . . . . . . 9 (𝐵𝐴 → (𝐴𝑥𝐵𝑥))
68 ensym 9063 . . . . . . . . 9 (𝐵𝑥𝑥𝐵)
6967, 68syl6com 37 . . . . . . . 8 (𝐴𝑥 → (𝐵𝐴𝑥𝐵))
7069ad2antlr 726 . . . . . . 7 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → (𝐵𝐴𝑥𝐵))
7165, 70mtod 198 . . . . . 6 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → ¬ 𝐵𝐴)
72 brsdom 9035 . . . . . 6 (𝐵𝐴 ↔ (𝐵𝐴 ∧ ¬ 𝐵𝐴))
738, 71, 72sylanbrc 582 . . . . 5 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → 𝐵𝐴)
7473exp31 419 . . . 4 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴𝐵𝐴)))
7574rexlimiv 3154 . . 3 (∃𝑥 ∈ ω 𝐴𝑥 → (𝐵𝐴𝐵𝐴))
761, 75sylbi 217 . 2 (𝐴 ∈ Fin → (𝐵𝐴𝐵𝐴))
7776imp 406 1 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wex 1777  wcel 2108  wrex 3076  Vcvv 3488  cdif 3973  wss 3976  wpss 3977  c0 4352   class class class wbr 5166  ccnv 5699  dom cdm 5700  ran crn 5701  cres 5702  cima 5703  Fun wfun 6567   Fn wfn 6568  1-1wf1 6570  ontowfo 6571  1-1-ontowf1o 6572  cfv 6573  ωcom 7903  cen 9000  cdom 9001  csdm 9002  Fincfn 9003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-om 7904  df-1o 8522  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator