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

Theorem php3OLD 9221
Description: Obsolete version of php3 9209 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 8969 . . 3 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
2 relen 8941 . . . . . . . . 9 Rel ≈
32brrelex1i 5723 . . . . . . . 8 (𝐴𝑥𝐴 ∈ V)
4 pssss 4088 . . . . . . . 8 (𝐵𝐴𝐵𝐴)
5 ssdomg 8993 . . . . . . . . 9 (𝐴 ∈ V → (𝐵𝐴𝐵𝐴))
65imp 406 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐵𝐴) → 𝐵𝐴)
73, 4, 6syl2an 595 . . . . . . 7 ((𝐴𝑥𝐵𝐴) → 𝐵𝐴)
87adantll 711 . . . . . 6 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → 𝐵𝐴)
9 bren 8946 . . . . . . . . 9 (𝐴𝑥 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝑥)
10 imass2 6092 . . . . . . . . . . . . . . . . 17 (𝐵𝐴 → (𝑓𝐵) ⊆ (𝑓𝐴))
114, 10syl 17 . . . . . . . . . . . . . . . 16 (𝐵𝐴 → (𝑓𝐵) ⊆ (𝑓𝐴))
1211adantl 481 . . . . . . . . . . . . . . 15 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊆ (𝑓𝐴))
13 pssnel 4463 . . . . . . . . . . . . . . . . 17 (𝐵𝐴 → ∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵))
14 eldif 3951 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴 ∧ ¬ 𝑦𝐵))
15 f1ofn 6825 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝐴1-1-onto𝑥𝑓 Fn 𝐴)
16 difss 4124 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴𝐵) ⊆ 𝐴
17 fnfvima 7227 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓 Fn 𝐴 ∧ (𝐴𝐵) ⊆ 𝐴𝑦 ∈ (𝐴𝐵)) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵)))
18173expia 1118 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 Fn 𝐴 ∧ (𝐴𝐵) ⊆ 𝐴) → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵))))
1915, 16, 18sylancl 585 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵))))
20 dff1o3 6830 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:𝐴1-1-onto𝑥 ↔ (𝑓:𝐴onto𝑥 ∧ Fun 𝑓))
21 imadif 6623 . . . . . . . . . . . . . . . . . . . . . . . 24 (Fun 𝑓 → (𝑓 “ (𝐴𝐵)) = ((𝑓𝐴) ∖ (𝑓𝐵)))
2220, 21simplbiim 504 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝐴1-1-onto𝑥 → (𝑓 “ (𝐴𝐵)) = ((𝑓𝐴) ∖ (𝑓𝐵)))
2322eleq2d 2811 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:𝐴1-1-onto𝑥 → ((𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵)) ↔ (𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵))))
2419, 23sylibd 238 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵))))
25 n0i 4326 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵)) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
2624, 25syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2714, 26biimtrrid 242 . . . . . . . . . . . . . . . . . . 19 (𝑓:𝐴1-1-onto𝑥 → ((𝑦𝐴 ∧ ¬ 𝑦𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2827exlimdv 1928 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴1-1-onto𝑥 → (∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2928imp 406 . . . . . . . . . . . . . . . . 17 ((𝑓:𝐴1-1-onto𝑥 ∧ ∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵)) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
3013, 29sylan2 592 . . . . . . . . . . . . . . . 16 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
31 ssdif0 4356 . . . . . . . . . . . . . . . 16 ((𝑓𝐴) ⊆ (𝑓𝐵) ↔ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
3230, 31sylnibr 329 . . . . . . . . . . . . . . 15 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ¬ (𝑓𝐴) ⊆ (𝑓𝐵))
33 dfpss3 4079 . . . . . . . . . . . . . . 15 ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ ((𝑓𝐵) ⊆ (𝑓𝐴) ∧ ¬ (𝑓𝐴) ⊆ (𝑓𝐵)))
3412, 32, 33sylanbrc 582 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊊ (𝑓𝐴))
35 imadmrn 6060 . . . . . . . . . . . . . . . . 17 (𝑓 “ dom 𝑓) = ran 𝑓
36 f1odm 6828 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴1-1-onto𝑥 → dom 𝑓 = 𝐴)
3736imaeq2d 6050 . . . . . . . . . . . . . . . . 17 (𝑓:𝐴1-1-onto𝑥 → (𝑓 “ dom 𝑓) = (𝑓𝐴))
38 f1ofo 6831 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴1-1-onto𝑥𝑓:𝐴onto𝑥)
39 forn 6799 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴onto𝑥 → ran 𝑓 = 𝑥)
4038, 39syl 17 . . . . . . . . . . . . . . . . 17 (𝑓:𝐴1-1-onto𝑥 → ran 𝑓 = 𝑥)
4135, 37, 403eqtr3a 2788 . . . . . . . . . . . . . . . 16 (𝑓:𝐴1-1-onto𝑥 → (𝑓𝐴) = 𝑥)
4241psseq2d 4086 . . . . . . . . . . . . . . 15 (𝑓:𝐴1-1-onto𝑥 → ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ (𝑓𝐵) ⊊ 𝑥))
4342adantr 480 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ (𝑓𝐵) ⊊ 𝑥))
4434, 43mpbid 231 . . . . . . . . . . . . 13 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊊ 𝑥)
45 php 9207 . . . . . . . . . . . . 13 ((𝑥 ∈ ω ∧ (𝑓𝐵) ⊊ 𝑥) → ¬ 𝑥 ≈ (𝑓𝐵))
4644, 45sylan2 592 . . . . . . . . . . . 12 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → ¬ 𝑥 ≈ (𝑓𝐵))
47 f1of1 6823 . . . . . . . . . . . . . . . 16 (𝑓:𝐴1-1-onto𝑥𝑓:𝐴1-1𝑥)
48 f1ores 6838 . . . . . . . . . . . . . . . 16 ((𝑓:𝐴1-1𝑥𝐵𝐴) → (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵))
4947, 4, 48syl2an 595 . . . . . . . . . . . . . . 15 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵))
50 vex 3470 . . . . . . . . . . . . . . . . . 18 𝑓 ∈ V
5150resex 6020 . . . . . . . . . . . . . . . . 17 (𝑓𝐵) ∈ V
52 f1oeq1 6812 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑓𝐵) → (𝑦:𝐵1-1-onto→(𝑓𝐵) ↔ (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵)))
5351, 52spcev 3588 . . . . . . . . . . . . . . . 16 ((𝑓𝐵):𝐵1-1-onto→(𝑓𝐵) → ∃𝑦 𝑦:𝐵1-1-onto→(𝑓𝐵))
54 bren 8946 . . . . . . . . . . . . . . . 16 (𝐵 ≈ (𝑓𝐵) ↔ ∃𝑦 𝑦:𝐵1-1-onto→(𝑓𝐵))
5553, 54sylibr 233 . . . . . . . . . . . . . . 15 ((𝑓𝐵):𝐵1-1-onto→(𝑓𝐵) → 𝐵 ≈ (𝑓𝐵))
5649, 55syl 17 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → 𝐵 ≈ (𝑓𝐵))
57 entr 8999 . . . . . . . . . . . . . . 15 ((𝑥𝐵𝐵 ≈ (𝑓𝐵)) → 𝑥 ≈ (𝑓𝐵))
5857expcom 413 . . . . . . . . . . . . . 14 (𝐵 ≈ (𝑓𝐵) → (𝑥𝐵𝑥 ≈ (𝑓𝐵)))
5956, 58syl 17 . . . . . . . . . . . . 13 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑥𝐵𝑥 ≈ (𝑓𝐵)))
6059adantl 481 . . . . . . . . . . . 12 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → (𝑥𝐵𝑥 ≈ (𝑓𝐵)))
6146, 60mtod 197 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → ¬ 𝑥𝐵)
6261exp32 420 . . . . . . . . . 10 (𝑥 ∈ ω → (𝑓:𝐴1-1-onto𝑥 → (𝐵𝐴 → ¬ 𝑥𝐵)))
6362exlimdv 1928 . . . . . . . . 9 (𝑥 ∈ ω → (∃𝑓 𝑓:𝐴1-1-onto𝑥 → (𝐵𝐴 → ¬ 𝑥𝐵)))
649, 63biimtrid 241 . . . . . . . 8 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴 → ¬ 𝑥𝐵)))
6564imp31 417 . . . . . . 7 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → ¬ 𝑥𝐵)
66 entr 8999 . . . . . . . . . 10 ((𝐵𝐴𝐴𝑥) → 𝐵𝑥)
6766ex 412 . . . . . . . . 9 (𝐵𝐴 → (𝐴𝑥𝐵𝑥))
68 ensym 8996 . . . . . . . . 9 (𝐵𝑥𝑥𝐵)
6967, 68syl6com 37 . . . . . . . 8 (𝐴𝑥 → (𝐵𝐴𝑥𝐵))
7069ad2antlr 724 . . . . . . 7 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → (𝐵𝐴𝑥𝐵))
7165, 70mtod 197 . . . . . 6 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → ¬ 𝐵𝐴)
72 brsdom 8968 . . . . . 6 (𝐵𝐴 ↔ (𝐵𝐴 ∧ ¬ 𝐵𝐴))
738, 71, 72sylanbrc 582 . . . . 5 (((𝑥 ∈ ω ∧ 𝐴𝑥) ∧ 𝐵𝐴) → 𝐵𝐴)
7473exp31 419 . . . 4 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴𝐵𝐴)))
7574rexlimiv 3140 . . 3 (∃𝑥 ∈ ω 𝐴𝑥 → (𝐵𝐴𝐵𝐴))
761, 75sylbi 216 . 2 (𝐴 ∈ Fin → (𝐵𝐴𝐵𝐴))
7776imp 406 1 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1533  wex 1773  wcel 2098  wrex 3062  Vcvv 3466  cdif 3938  wss 3941  wpss 3942  c0 4315   class class class wbr 5139  ccnv 5666  dom cdm 5667  ran crn 5668  cres 5669  cima 5670  Fun wfun 6528   Fn wfn 6529  1-1wf1 6531  ontowfo 6532  1-1-ontowf1o 6533  cfv 6534  ωcom 7849  cen 8933  cdom 8934  csdm 8935  Fincfn 8936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-om 7850  df-1o 8462  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator