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

Theorem en2lp 4232
Description: No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206. (Contributed by NM, 16-Oct-1996.) (Proof rewritten by Mario Carneiro and Jim Kingdon, 27-Nov-2018.)
Assertion
Ref Expression
en2lp ¬ (A B B A)

Proof of Theorem en2lp
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2560 . . . . . . . . . . . 12 (B AB V)
2 prid2g 3466 . . . . . . . . . . . . 13 (B V → B {A, B})
3 eldif 2921 . . . . . . . . . . . . . . 15 (B (V ∖ {A, B}) ↔ (B V ¬ B {A, B}))
4 pm3.4 316 . . . . . . . . . . . . . . 15 ((B V ¬ B {A, B}) → (B V → ¬ B {A, B}))
53, 4sylbi 114 . . . . . . . . . . . . . 14 (B (V ∖ {A, B}) → (B V → ¬ B {A, B}))
65com12 27 . . . . . . . . . . . . 13 (B V → (B (V ∖ {A, B}) → ¬ B {A, B}))
72, 6mt2d 555 . . . . . . . . . . . 12 (B V → ¬ B (V ∖ {A, B}))
81, 7syl 14 . . . . . . . . . . 11 (B A → ¬ B (V ∖ {A, B}))
98ad2antlr 458 . . . . . . . . . 10 (((A B B A) y(y xy (V ∖ {A, B}))) → ¬ B (V ∖ {A, B}))
10 simp1r 928 . . . . . . . . . . . 12 (((A B B A) y(y xy (V ∖ {A, B})) x = A) → B A)
11 eleq1 2097 . . . . . . . . . . . . . . . . 17 (y = B → (y xB x))
12 eleq1 2097 . . . . . . . . . . . . . . . . 17 (y = B → (y (V ∖ {A, B}) ↔ B (V ∖ {A, B})))
1311, 12imbi12d 223 . . . . . . . . . . . . . . . 16 (y = B → ((y xy (V ∖ {A, B})) ↔ (B xB (V ∖ {A, B}))))
1413spcgv 2634 . . . . . . . . . . . . . . 15 (B x → (y(y xy (V ∖ {A, B})) → (B xB (V ∖ {A, B}))))
1514pm2.43b 46 . . . . . . . . . . . . . 14 (y(y xy (V ∖ {A, B})) → (B xB (V ∖ {A, B})))
16153ad2ant2 925 . . . . . . . . . . . . 13 (((A B B A) y(y xy (V ∖ {A, B})) x = A) → (B xB (V ∖ {A, B})))
17 eleq2 2098 . . . . . . . . . . . . . . 15 (x = A → (B xB A))
1817imbi1d 220 . . . . . . . . . . . . . 14 (x = A → ((B xB (V ∖ {A, B})) ↔ (B AB (V ∖ {A, B}))))
19183ad2ant3 926 . . . . . . . . . . . . 13 (((A B B A) y(y xy (V ∖ {A, B})) x = A) → ((B xB (V ∖ {A, B})) ↔ (B AB (V ∖ {A, B}))))
2016, 19mpbid 135 . . . . . . . . . . . 12 (((A B B A) y(y xy (V ∖ {A, B})) x = A) → (B AB (V ∖ {A, B})))
2110, 20mpd 13 . . . . . . . . . . 11 (((A B B A) y(y xy (V ∖ {A, B})) x = A) → B (V ∖ {A, B}))
22213expia 1105 . . . . . . . . . 10 (((A B B A) y(y xy (V ∖ {A, B}))) → (x = AB (V ∖ {A, B})))
239, 22mtod 588 . . . . . . . . 9 (((A B B A) y(y xy (V ∖ {A, B}))) → ¬ x = A)
24 elex 2560 . . . . . . . . . . . . 13 (A BA V)
25 prid1g 3465 . . . . . . . . . . . . . 14 (A V → A {A, B})
26 eldif 2921 . . . . . . . . . . . . . . . 16 (A (V ∖ {A, B}) ↔ (A V ¬ A {A, B}))
27 pm3.4 316 . . . . . . . . . . . . . . . 16 ((A V ¬ A {A, B}) → (A V → ¬ A {A, B}))
2826, 27sylbi 114 . . . . . . . . . . . . . . 15 (A (V ∖ {A, B}) → (A V → ¬ A {A, B}))
2928com12 27 . . . . . . . . . . . . . 14 (A V → (A (V ∖ {A, B}) → ¬ A {A, B}))
3025, 29mt2d 555 . . . . . . . . . . . . 13 (A V → ¬ A (V ∖ {A, B}))
3124, 30syl 14 . . . . . . . . . . . 12 (A B → ¬ A (V ∖ {A, B}))
3231adantr 261 . . . . . . . . . . 11 ((A B B A) → ¬ A (V ∖ {A, B}))
3332adantr 261 . . . . . . . . . 10 (((A B B A) y(y xy (V ∖ {A, B}))) → ¬ A (V ∖ {A, B}))
34 simp1l 927 . . . . . . . . . . . 12 (((A B B A) y(y xy (V ∖ {A, B})) x = B) → A B)
35 eleq1 2097 . . . . . . . . . . . . . . . . 17 (y = A → (y xA x))
36 eleq1 2097 . . . . . . . . . . . . . . . . 17 (y = A → (y (V ∖ {A, B}) ↔ A (V ∖ {A, B})))
3735, 36imbi12d 223 . . . . . . . . . . . . . . . 16 (y = A → ((y xy (V ∖ {A, B})) ↔ (A xA (V ∖ {A, B}))))
3837spcgv 2634 . . . . . . . . . . . . . . 15 (A x → (y(y xy (V ∖ {A, B})) → (A xA (V ∖ {A, B}))))
3938pm2.43b 46 . . . . . . . . . . . . . 14 (y(y xy (V ∖ {A, B})) → (A xA (V ∖ {A, B})))
40393ad2ant2 925 . . . . . . . . . . . . 13 (((A B B A) y(y xy (V ∖ {A, B})) x = B) → (A xA (V ∖ {A, B})))
41 eleq2 2098 . . . . . . . . . . . . . . 15 (x = B → (A xA B))
4241imbi1d 220 . . . . . . . . . . . . . 14 (x = B → ((A xA (V ∖ {A, B})) ↔ (A BA (V ∖ {A, B}))))
43423ad2ant3 926 . . . . . . . . . . . . 13 (((A B B A) y(y xy (V ∖ {A, B})) x = B) → ((A xA (V ∖ {A, B})) ↔ (A BA (V ∖ {A, B}))))
4440, 43mpbid 135 . . . . . . . . . . . 12 (((A B B A) y(y xy (V ∖ {A, B})) x = B) → (A BA (V ∖ {A, B})))
4534, 44mpd 13 . . . . . . . . . . 11 (((A B B A) y(y xy (V ∖ {A, B})) x = B) → A (V ∖ {A, B}))
46453expia 1105 . . . . . . . . . 10 (((A B B A) y(y xy (V ∖ {A, B}))) → (x = BA (V ∖ {A, B})))
4733, 46mtod 588 . . . . . . . . 9 (((A B B A) y(y xy (V ∖ {A, B}))) → ¬ x = B)
48 ioran 668 . . . . . . . . 9 (¬ (x = A x = B) ↔ (¬ x = A ¬ x = B))
4923, 47, 48sylanbrc 394 . . . . . . . 8 (((A B B A) y(y xy (V ∖ {A, B}))) → ¬ (x = A x = B))
50 vex 2554 . . . . . . . . . 10 x V
51 eldif 2921 . . . . . . . . . 10 (x (V ∖ {A, B}) ↔ (x V ¬ x {A, B}))
5250, 51mpbiran 846 . . . . . . . . 9 (x (V ∖ {A, B}) ↔ ¬ x {A, B})
5350elpr 3385 . . . . . . . . 9 (x {A, B} ↔ (x = A x = B))
5452, 53xchbinx 606 . . . . . . . 8 (x (V ∖ {A, B}) ↔ ¬ (x = A x = B))
5549, 54sylibr 137 . . . . . . 7 (((A B B A) y(y xy (V ∖ {A, B}))) → x (V ∖ {A, B}))
5655ex 108 . . . . . 6 ((A B B A) → (y(y xy (V ∖ {A, B})) → x (V ∖ {A, B})))
5756alrimiv 1751 . . . . 5 ((A B B A) → x(y(y xy (V ∖ {A, B})) → x (V ∖ {A, B})))
58 df-ral 2305 . . . . . . . 8 (y x [y / x]x (V ∖ {A, B}) ↔ y(y x → [y / x]x (V ∖ {A, B})))
59 clelsb3 2139 . . . . . . . . . 10 ([y / x]x (V ∖ {A, B}) ↔ y (V ∖ {A, B}))
6059imbi2i 215 . . . . . . . . 9 ((y x → [y / x]x (V ∖ {A, B})) ↔ (y xy (V ∖ {A, B})))
6160albii 1356 . . . . . . . 8 (y(y x → [y / x]x (V ∖ {A, B})) ↔ y(y xy (V ∖ {A, B})))
6258, 61bitri 173 . . . . . . 7 (y x [y / x]x (V ∖ {A, B}) ↔ y(y xy (V ∖ {A, B})))
6362imbi1i 227 . . . . . 6 ((y x [y / x]x (V ∖ {A, B}) → x (V ∖ {A, B})) ↔ (y(y xy (V ∖ {A, B})) → x (V ∖ {A, B})))
6463albii 1356 . . . . 5 (x(y x [y / x]x (V ∖ {A, B}) → x (V ∖ {A, B})) ↔ x(y(y xy (V ∖ {A, B})) → x (V ∖ {A, B})))
6557, 64sylibr 137 . . . 4 ((A B B A) → x(y x [y / x]x (V ∖ {A, B}) → x (V ∖ {A, B})))
66 ax-setind 4220 . . . 4 (x(y x [y / x]x (V ∖ {A, B}) → x (V ∖ {A, B})) → x x (V ∖ {A, B}))
6765, 66syl 14 . . 3 ((A B B A) → x x (V ∖ {A, B}))
68 eleq1 2097 . . . . 5 (x = A → (x (V ∖ {A, B}) ↔ A (V ∖ {A, B})))
6968spcgv 2634 . . . 4 (A B → (x x (V ∖ {A, B}) → A (V ∖ {A, B})))
7069adantr 261 . . 3 ((A B B A) → (x x (V ∖ {A, B}) → A (V ∖ {A, B})))
7167, 70mpd 13 . 2 ((A B B A) → A (V ∖ {A, B}))
7271, 32pm2.65i 567 1 ¬ (A B B A)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98   wo 628   w3a 884  wal 1240   = wceq 1242   wcel 1390  [wsb 1642  wral 2300  Vcvv 2551  cdif 2908  {cpr 3368
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-in1 544  ax-in2 545  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-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-setind 4220
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-v 2553  df-dif 2914  df-un 2916  df-sn 3373  df-pr 3374
This theorem is referenced by:  preleq  4233  suc11g  4235  ordsuc  4241  2pwuninelg  5839  nntri2  6012  nndcel  6016
  Copyright terms: Public domain W3C validator