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

Theorem ssfin4 10246
Description: Dedekind finite sets have Dedekind finite subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 6-May-2015.) (Revised by Mario Carneiro, 16-May-2015.)
Assertion
Ref Expression
ssfin4 ((𝐴 ∈ FinIV𝐵𝐴) → 𝐵 ∈ FinIV)

Proof of Theorem ssfin4
Dummy variables 𝑐 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 765 . . . 4 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → 𝐴 ∈ FinIV)
2 pssss 4055 . . . . . . . . 9 (𝑥𝐵𝑥𝐵)
3 simpr 485 . . . . . . . . 9 ((𝐴 ∈ FinIV𝐵𝐴) → 𝐵𝐴)
42, 3sylan9ssr 3958 . . . . . . . 8 (((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) → 𝑥𝐴)
5 difssd 4092 . . . . . . . 8 (((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) → (𝐴𝐵) ⊆ 𝐴)
64, 5unssd 4146 . . . . . . 7 (((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) → (𝑥 ∪ (𝐴𝐵)) ⊆ 𝐴)
7 pssnel 4430 . . . . . . . . 9 (𝑥𝐵 → ∃𝑐(𝑐𝐵 ∧ ¬ 𝑐𝑥))
87adantl 482 . . . . . . . 8 (((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) → ∃𝑐(𝑐𝐵 ∧ ¬ 𝑐𝑥))
9 simpllr 774 . . . . . . . . . . 11 ((((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) ∧ (𝑐𝐵 ∧ ¬ 𝑐𝑥)) → 𝐵𝐴)
10 simprl 769 . . . . . . . . . . 11 ((((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) ∧ (𝑐𝐵 ∧ ¬ 𝑐𝑥)) → 𝑐𝐵)
119, 10sseldd 3945 . . . . . . . . . 10 ((((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) ∧ (𝑐𝐵 ∧ ¬ 𝑐𝑥)) → 𝑐𝐴)
12 simprr 771 . . . . . . . . . . 11 ((((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) ∧ (𝑐𝐵 ∧ ¬ 𝑐𝑥)) → ¬ 𝑐𝑥)
13 elndif 4088 . . . . . . . . . . . 12 (𝑐𝐵 → ¬ 𝑐 ∈ (𝐴𝐵))
1413ad2antrl 726 . . . . . . . . . . 11 ((((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) ∧ (𝑐𝐵 ∧ ¬ 𝑐𝑥)) → ¬ 𝑐 ∈ (𝐴𝐵))
15 ioran 982 . . . . . . . . . . . 12 (¬ (𝑐𝑥𝑐 ∈ (𝐴𝐵)) ↔ (¬ 𝑐𝑥 ∧ ¬ 𝑐 ∈ (𝐴𝐵)))
16 elun 4108 . . . . . . . . . . . 12 (𝑐 ∈ (𝑥 ∪ (𝐴𝐵)) ↔ (𝑐𝑥𝑐 ∈ (𝐴𝐵)))
1715, 16xchnxbir 332 . . . . . . . . . . 11 𝑐 ∈ (𝑥 ∪ (𝐴𝐵)) ↔ (¬ 𝑐𝑥 ∧ ¬ 𝑐 ∈ (𝐴𝐵)))
1812, 14, 17sylanbrc 583 . . . . . . . . . 10 ((((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) ∧ (𝑐𝐵 ∧ ¬ 𝑐𝑥)) → ¬ 𝑐 ∈ (𝑥 ∪ (𝐴𝐵)))
19 nelneq2 2862 . . . . . . . . . 10 ((𝑐𝐴 ∧ ¬ 𝑐 ∈ (𝑥 ∪ (𝐴𝐵))) → ¬ 𝐴 = (𝑥 ∪ (𝐴𝐵)))
2011, 18, 19syl2anc 584 . . . . . . . . 9 ((((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) ∧ (𝑐𝐵 ∧ ¬ 𝑐𝑥)) → ¬ 𝐴 = (𝑥 ∪ (𝐴𝐵)))
21 eqcom 2743 . . . . . . . . 9 (𝐴 = (𝑥 ∪ (𝐴𝐵)) ↔ (𝑥 ∪ (𝐴𝐵)) = 𝐴)
2220, 21sylnib 327 . . . . . . . 8 ((((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) ∧ (𝑐𝐵 ∧ ¬ 𝑐𝑥)) → ¬ (𝑥 ∪ (𝐴𝐵)) = 𝐴)
238, 22exlimddv 1938 . . . . . . 7 (((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) → ¬ (𝑥 ∪ (𝐴𝐵)) = 𝐴)
24 dfpss2 4045 . . . . . . 7 ((𝑥 ∪ (𝐴𝐵)) ⊊ 𝐴 ↔ ((𝑥 ∪ (𝐴𝐵)) ⊆ 𝐴 ∧ ¬ (𝑥 ∪ (𝐴𝐵)) = 𝐴))
256, 23, 24sylanbrc 583 . . . . . 6 (((𝐴 ∈ FinIV𝐵𝐴) ∧ 𝑥𝐵) → (𝑥 ∪ (𝐴𝐵)) ⊊ 𝐴)
2625adantrr 715 . . . . 5 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → (𝑥 ∪ (𝐴𝐵)) ⊊ 𝐴)
27 simprr 771 . . . . . . 7 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → 𝑥𝐵)
28 difexg 5284 . . . . . . . 8 (𝐴 ∈ FinIV → (𝐴𝐵) ∈ V)
29 enrefg 8924 . . . . . . . 8 ((𝐴𝐵) ∈ V → (𝐴𝐵) ≈ (𝐴𝐵))
301, 28, 293syl 18 . . . . . . 7 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → (𝐴𝐵) ≈ (𝐴𝐵))
312ad2antrl 726 . . . . . . . . . 10 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → 𝑥𝐵)
32 ssinss1 4197 . . . . . . . . . 10 (𝑥𝐵 → (𝑥𝐴) ⊆ 𝐵)
3331, 32syl 17 . . . . . . . . 9 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → (𝑥𝐴) ⊆ 𝐵)
34 inssdif0 4329 . . . . . . . . 9 ((𝑥𝐴) ⊆ 𝐵 ↔ (𝑥 ∩ (𝐴𝐵)) = ∅)
3533, 34sylib 217 . . . . . . . 8 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → (𝑥 ∩ (𝐴𝐵)) = ∅)
36 disjdif 4431 . . . . . . . 8 (𝐵 ∩ (𝐴𝐵)) = ∅
3735, 36jctir 521 . . . . . . 7 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → ((𝑥 ∩ (𝐴𝐵)) = ∅ ∧ (𝐵 ∩ (𝐴𝐵)) = ∅))
38 unen 8990 . . . . . . 7 (((𝑥𝐵 ∧ (𝐴𝐵) ≈ (𝐴𝐵)) ∧ ((𝑥 ∩ (𝐴𝐵)) = ∅ ∧ (𝐵 ∩ (𝐴𝐵)) = ∅)) → (𝑥 ∪ (𝐴𝐵)) ≈ (𝐵 ∪ (𝐴𝐵)))
3927, 30, 37, 38syl21anc 836 . . . . . 6 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → (𝑥 ∪ (𝐴𝐵)) ≈ (𝐵 ∪ (𝐴𝐵)))
40 simplr 767 . . . . . . 7 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → 𝐵𝐴)
41 undif 4441 . . . . . . 7 (𝐵𝐴 ↔ (𝐵 ∪ (𝐴𝐵)) = 𝐴)
4240, 41sylib 217 . . . . . 6 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → (𝐵 ∪ (𝐴𝐵)) = 𝐴)
4339, 42breqtrd 5131 . . . . 5 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → (𝑥 ∪ (𝐴𝐵)) ≈ 𝐴)
44 fin4i 10234 . . . . 5 (((𝑥 ∪ (𝐴𝐵)) ⊊ 𝐴 ∧ (𝑥 ∪ (𝐴𝐵)) ≈ 𝐴) → ¬ 𝐴 ∈ FinIV)
4526, 43, 44syl2anc 584 . . . 4 (((𝐴 ∈ FinIV𝐵𝐴) ∧ (𝑥𝐵𝑥𝐵)) → ¬ 𝐴 ∈ FinIV)
461, 45pm2.65da 815 . . 3 ((𝐴 ∈ FinIV𝐵𝐴) → ¬ (𝑥𝐵𝑥𝐵))
4746nexdv 1939 . 2 ((𝐴 ∈ FinIV𝐵𝐴) → ¬ ∃𝑥(𝑥𝐵𝑥𝐵))
48 ssexg 5280 . . . 4 ((𝐵𝐴𝐴 ∈ FinIV) → 𝐵 ∈ V)
4948ancoms 459 . . 3 ((𝐴 ∈ FinIV𝐵𝐴) → 𝐵 ∈ V)
50 isfin4 10233 . . 3 (𝐵 ∈ V → (𝐵 ∈ FinIV ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐵)))
5149, 50syl 17 . 2 ((𝐴 ∈ FinIV𝐵𝐴) → (𝐵 ∈ FinIV ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐵)))
5247, 51mpbird 256 1 ((𝐴 ∈ FinIV𝐵𝐴) → 𝐵 ∈ FinIV)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wex 1781  wcel 2106  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  wpss 3911  c0 4282   class class class wbr 5105  cen 8880  FinIVcfin4 10216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-en 8884  df-fin4 10223
This theorem is referenced by:  domfin4  10247
  Copyright terms: Public domain W3C validator