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

Theorem en2lp 4333
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 ¬ (𝐴𝐵𝐵𝐴)

Proof of Theorem en2lp
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2621 . . . . . . . . . . . 12 (𝐵𝐴𝐵 ∈ V)
2 prid2g 3521 . . . . . . . . . . . . 13 (𝐵 ∈ V → 𝐵 ∈ {𝐴, 𝐵})
3 eldif 2993 . . . . . . . . . . . . . . 15 (𝐵 ∈ (V ∖ {𝐴, 𝐵}) ↔ (𝐵 ∈ V ∧ ¬ 𝐵 ∈ {𝐴, 𝐵}))
4 pm3.4 326 . . . . . . . . . . . . . . 15 ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ {𝐴, 𝐵}) → (𝐵 ∈ V → ¬ 𝐵 ∈ {𝐴, 𝐵}))
53, 4sylbi 119 . . . . . . . . . . . . . 14 (𝐵 ∈ (V ∖ {𝐴, 𝐵}) → (𝐵 ∈ V → ¬ 𝐵 ∈ {𝐴, 𝐵}))
65com12 30 . . . . . . . . . . . . 13 (𝐵 ∈ V → (𝐵 ∈ (V ∖ {𝐴, 𝐵}) → ¬ 𝐵 ∈ {𝐴, 𝐵}))
72, 6mt2d 588 . . . . . . . . . . . 12 (𝐵 ∈ V → ¬ 𝐵 ∈ (V ∖ {𝐴, 𝐵}))
81, 7syl 14 . . . . . . . . . . 11 (𝐵𝐴 → ¬ 𝐵 ∈ (V ∖ {𝐴, 𝐵}))
98ad2antlr 473 . . . . . . . . . 10 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ 𝐵 ∈ (V ∖ {𝐴, 𝐵}))
10 simp1r 964 . . . . . . . . . . . 12 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → 𝐵𝐴)
11 eleq1 2145 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐵 → (𝑦𝑥𝐵𝑥))
12 eleq1 2145 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐵 → (𝑦 ∈ (V ∖ {𝐴, 𝐵}) ↔ 𝐵 ∈ (V ∖ {𝐴, 𝐵})))
1311, 12imbi12d 232 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵 → ((𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵}))))
1413spcgv 2696 . . . . . . . . . . . . . . 15 (𝐵𝑥 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → (𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵}))))
1514pm2.43b 51 . . . . . . . . . . . . . 14 (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → (𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵})))
16153ad2ant2 961 . . . . . . . . . . . . 13 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → (𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵})))
17 eleq2 2146 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → (𝐵𝑥𝐵𝐴))
1817imbi1d 229 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → ((𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐵𝐴𝐵 ∈ (V ∖ {𝐴, 𝐵}))))
19183ad2ant3 962 . . . . . . . . . . . . 13 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → ((𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐵𝐴𝐵 ∈ (V ∖ {𝐴, 𝐵}))))
2016, 19mpbid 145 . . . . . . . . . . . 12 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → (𝐵𝐴𝐵 ∈ (V ∖ {𝐴, 𝐵})))
2110, 20mpd 13 . . . . . . . . . . 11 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → 𝐵 ∈ (V ∖ {𝐴, 𝐵}))
22213expia 1141 . . . . . . . . . 10 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → (𝑥 = 𝐴𝐵 ∈ (V ∖ {𝐴, 𝐵})))
239, 22mtod 622 . . . . . . . . 9 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ 𝑥 = 𝐴)
24 elex 2621 . . . . . . . . . . . . 13 (𝐴𝐵𝐴 ∈ V)
25 prid1g 3520 . . . . . . . . . . . . . 14 (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
26 eldif 2993 . . . . . . . . . . . . . . . 16 (𝐴 ∈ (V ∖ {𝐴, 𝐵}) ↔ (𝐴 ∈ V ∧ ¬ 𝐴 ∈ {𝐴, 𝐵}))
27 pm3.4 326 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ V ∧ ¬ 𝐴 ∈ {𝐴, 𝐵}) → (𝐴 ∈ V → ¬ 𝐴 ∈ {𝐴, 𝐵}))
2826, 27sylbi 119 . . . . . . . . . . . . . . 15 (𝐴 ∈ (V ∖ {𝐴, 𝐵}) → (𝐴 ∈ V → ¬ 𝐴 ∈ {𝐴, 𝐵}))
2928com12 30 . . . . . . . . . . . . . 14 (𝐴 ∈ V → (𝐴 ∈ (V ∖ {𝐴, 𝐵}) → ¬ 𝐴 ∈ {𝐴, 𝐵}))
3025, 29mt2d 588 . . . . . . . . . . . . 13 (𝐴 ∈ V → ¬ 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
3124, 30syl 14 . . . . . . . . . . . 12 (𝐴𝐵 → ¬ 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
3231adantr 270 . . . . . . . . . . 11 ((𝐴𝐵𝐵𝐴) → ¬ 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
3332adantr 270 . . . . . . . . . 10 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
34 simp1l 963 . . . . . . . . . . . 12 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → 𝐴𝐵)
35 eleq1 2145 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
36 eleq1 2145 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴, 𝐵}) ↔ 𝐴 ∈ (V ∖ {𝐴, 𝐵})))
3735, 36imbi12d 232 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → ((𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵}))))
3837spcgv 2696 . . . . . . . . . . . . . . 15 (𝐴𝑥 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵}))))
3938pm2.43b 51 . . . . . . . . . . . . . 14 (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵})))
40393ad2ant2 961 . . . . . . . . . . . . 13 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵})))
41 eleq2 2146 . . . . . . . . . . . . . . 15 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
4241imbi1d 229 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐴𝐵𝐴 ∈ (V ∖ {𝐴, 𝐵}))))
43423ad2ant3 962 . . . . . . . . . . . . 13 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐴𝐵𝐴 ∈ (V ∖ {𝐴, 𝐵}))))
4440, 43mpbid 145 . . . . . . . . . . . 12 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → (𝐴𝐵𝐴 ∈ (V ∖ {𝐴, 𝐵})))
4534, 44mpd 13 . . . . . . . . . . 11 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
46453expia 1141 . . . . . . . . . 10 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → (𝑥 = 𝐵𝐴 ∈ (V ∖ {𝐴, 𝐵})))
4733, 46mtod 622 . . . . . . . . 9 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ 𝑥 = 𝐵)
48 ioran 702 . . . . . . . . 9 (¬ (𝑥 = 𝐴𝑥 = 𝐵) ↔ (¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵))
4923, 47, 48sylanbrc 408 . . . . . . . 8 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ (𝑥 = 𝐴𝑥 = 𝐵))
50 vex 2615 . . . . . . . . . 10 𝑥 ∈ V
51 eldif 2993 . . . . . . . . . 10 (𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴, 𝐵}))
5250, 51mpbiran 882 . . . . . . . . 9 (𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ ¬ 𝑥 ∈ {𝐴, 𝐵})
5350elpr 3443 . . . . . . . . 9 (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴𝑥 = 𝐵))
5452, 53xchbinx 640 . . . . . . . 8 (𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ ¬ (𝑥 = 𝐴𝑥 = 𝐵))
5549, 54sylibr 132 . . . . . . 7 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → 𝑥 ∈ (V ∖ {𝐴, 𝐵}))
5655ex 113 . . . . . 6 ((𝐴𝐵𝐵𝐴) → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
5756alrimiv 1797 . . . . 5 ((𝐴𝐵𝐵𝐴) → ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
58 df-ral 2358 . . . . . . . 8 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ ∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵})))
59 clelsb3 2187 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ 𝑦 ∈ (V ∖ {𝐴, 𝐵}))
6059imbi2i 224 . . . . . . . . 9 ((𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})))
6160albii 1400 . . . . . . . 8 (∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵})) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})))
6258, 61bitri 182 . . . . . . 7 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})))
6362imbi1i 236 . . . . . 6 ((∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})) ↔ (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
6463albii 1400 . . . . 5 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})) ↔ ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
6557, 64sylibr 132 . . . 4 ((𝐴𝐵𝐵𝐴) → ∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
66 ax-setind 4316 . . . 4 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴, 𝐵}))
6765, 66syl 14 . . 3 ((𝐴𝐵𝐵𝐴) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴, 𝐵}))
68 eleq1 2145 . . . . 5 (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ 𝐴 ∈ (V ∖ {𝐴, 𝐵})))
6968spcgv 2696 . . . 4 (𝐴𝐵 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝐴 ∈ (V ∖ {𝐴, 𝐵})))
7069adantr 270 . . 3 ((𝐴𝐵𝐵𝐴) → (∀𝑥 𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝐴 ∈ (V ∖ {𝐴, 𝐵})))
7167, 70mpd 13 . 2 ((𝐴𝐵𝐵𝐴) → 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
7271, 32pm2.65i 601 1 ¬ (𝐴𝐵𝐵𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662  w3a 920  wal 1283   = wceq 1285  wcel 1434  [wsb 1687  wral 2353  Vcvv 2612  cdif 2981  {cpr 3423
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-setind 4316
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-v 2614  df-dif 2986  df-un 2988  df-sn 3428  df-pr 3429
This theorem is referenced by:  preleq  4334  suc11g  4336  ordsuc  4342  2pwuninelg  5980  nntri2  6187  nndcel  6193
  Copyright terms: Public domain W3C validator