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

Theorem en2lp 4212
 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 2539 . . . . . . . . . . . 12 (B AB V)
2 prid2g 3445 . . . . . . . . . . . . 13 (B V → B {A, B})
3 eldif 2900 . . . . . . . . . . . . . . 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 543 . . . . . . . . . . . 12 (B V → ¬ B (V ∖ {A, B}))
81, 7syl 14 . . . . . . . . . . 11 (B A → ¬ B (V ∖ {A, B}))
98ad2antlr 462 . . . . . . . . . 10 (((A B B A) y(y xy (V ∖ {A, B}))) → ¬ B (V ∖ {A, B}))
10 simp1r 915 . . . . . . . . . . . 12 (((A B B A) y(y xy (V ∖ {A, B})) x = A) → B A)
11 eleq1 2078 . . . . . . . . . . . . . . . . 17 (y = B → (y xB x))
12 eleq1 2078 . . . . . . . . . . . . . . . . 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 2613 . . . . . . . . . . . . . . 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 912 . . . . . . . . . . . . 13 (((A B B A) y(y xy (V ∖ {A, B})) x = A) → (B xB (V ∖ {A, B})))
17 eleq2 2079 . . . . . . . . . . . . . . 15 (x = A → (B xB A))
1817imbi1d 220 . . . . . . . . . . . . . 14 (x = A → ((B xB (V ∖ {A, B})) ↔ (B AB (V ∖ {A, B}))))
19183ad2ant3 913 . . . . . . . . . . . . 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 1090 . . . . . . . . . 10 (((A B B A) y(y xy (V ∖ {A, B}))) → (x = AB (V ∖ {A, B})))
239, 22mtod 576 . . . . . . . . 9 (((A B B A) y(y xy (V ∖ {A, B}))) → ¬ x = A)
24 elex 2539 . . . . . . . . . . . . 13 (A BA V)
25 prid1g 3444 . . . . . . . . . . . . . 14 (A V → A {A, B})
26 eldif 2900 . . . . . . . . . . . . . . . 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 543 . . . . . . . . . . . . 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 914 . . . . . . . . . . . 12 (((A B B A) y(y xy (V ∖ {A, B})) x = B) → A B)
35 eleq1 2078 . . . . . . . . . . . . . . . . 17 (y = A → (y xA x))
36 eleq1 2078 . . . . . . . . . . . . . . . . 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 2613 . . . . . . . . . . . . . . 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 912 . . . . . . . . . . . . 13 (((A B B A) y(y xy (V ∖ {A, B})) x = B) → (A xA (V ∖ {A, B})))
41 eleq2 2079 . . . . . . . . . . . . . . 15 (x = B → (A xA B))
4241imbi1d 220 . . . . . . . . . . . . . 14 (x = B → ((A xA (V ∖ {A, B})) ↔ (A BA (V ∖ {A, B}))))
43423ad2ant3 913 . . . . . . . . . . . . 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 1090 . . . . . . . . . 10 (((A B B A) y(y xy (V ∖ {A, B}))) → (x = BA (V ∖ {A, B})))
4733, 46mtod 576 . . . . . . . . 9 (((A B B A) y(y xy (V ∖ {A, B}))) → ¬ x = B)
48 ioran 656 . . . . . . . . 9 (¬ (x = A x = B) ↔ (¬ x = A ¬ x = B))
4923, 47, 48sylanbrc 396 . . . . . . . 8 (((A B B A) y(y xy (V ∖ {A, B}))) → ¬ (x = A x = B))
50 vex 2534 . . . . . . . . . 10 x V
51 eldif 2900 . . . . . . . . . 10 (x (V ∖ {A, B}) ↔ (x V ¬ x {A, B}))
5250, 51mpbiran 833 . . . . . . . . 9 (x (V ∖ {A, B}) ↔ ¬ x {A, B})
5350elpr 3364 . . . . . . . . 9 (x {A, B} ↔ (x = A x = B))
5452, 53xchbinx 594 . . . . . . . 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 1732 . . . . 5 ((A B B A) → x(y(y xy (V ∖ {A, B})) → x (V ∖ {A, B})))
58 df-ral 2285 . . . . . . . 8 (y x [y / x]x (V ∖ {A, B}) ↔ y(y x → [y / x]x (V ∖ {A, B})))
59 clelsb3 2120 . . . . . . . . . 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 1335 . . . . . . . 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 1335 . . . . 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 4200 . . . 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 2078 . . . . 5 (x = A → (x (V ∖ {A, B}) ↔ A (V ∖ {A, B})))
6968spcgv 2613 . . . 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 555 1 ¬ (A B B A)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616   ∧ w3a 871  ∀wal 1224   = wceq 1226   ∈ wcel 1370  [wsb 1623  ∀wral 2280  Vcvv 2531   ∖ cdif 2887  {cpr 3347 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 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-setind 4200 This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-v 2533  df-dif 2893  df-un 2895  df-sn 3352  df-pr 3353 This theorem is referenced by:  preleq  4213  suc11g  4215  ordsuc  4221  2pwuninelg  5816  nntri2  5984  nndcel  5987
 Copyright terms: Public domain W3C validator