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

Theorem en2lp 4278
 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 2566 . . . . . . . . . . . 12 (𝐵𝐴𝐵 ∈ V)
2 prid2g 3475 . . . . . . . . . . . . 13 (𝐵 ∈ V → 𝐵 ∈ {𝐴, 𝐵})
3 eldif 2927 . . . . . . . . . . . . . . 15 (𝐵 ∈ (V ∖ {𝐴, 𝐵}) ↔ (𝐵 ∈ V ∧ ¬ 𝐵 ∈ {𝐴, 𝐵}))
4 pm3.4 316 . . . . . . . . . . . . . . 15 ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ {𝐴, 𝐵}) → (𝐵 ∈ V → ¬ 𝐵 ∈ {𝐴, 𝐵}))
53, 4sylbi 114 . . . . . . . . . . . . . 14 (𝐵 ∈ (V ∖ {𝐴, 𝐵}) → (𝐵 ∈ V → ¬ 𝐵 ∈ {𝐴, 𝐵}))
65com12 27 . . . . . . . . . . . . 13 (𝐵 ∈ V → (𝐵 ∈ (V ∖ {𝐴, 𝐵}) → ¬ 𝐵 ∈ {𝐴, 𝐵}))
72, 6mt2d 555 . . . . . . . . . . . 12 (𝐵 ∈ V → ¬ 𝐵 ∈ (V ∖ {𝐴, 𝐵}))
81, 7syl 14 . . . . . . . . . . 11 (𝐵𝐴 → ¬ 𝐵 ∈ (V ∖ {𝐴, 𝐵}))
98ad2antlr 458 . . . . . . . . . 10 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ 𝐵 ∈ (V ∖ {𝐴, 𝐵}))
10 simp1r 929 . . . . . . . . . . . 12 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → 𝐵𝐴)
11 eleq1 2100 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐵 → (𝑦𝑥𝐵𝑥))
12 eleq1 2100 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐵 → (𝑦 ∈ (V ∖ {𝐴, 𝐵}) ↔ 𝐵 ∈ (V ∖ {𝐴, 𝐵})))
1311, 12imbi12d 223 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐵 → ((𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵}))))
1413spcgv 2640 . . . . . . . . . . . . . . 15 (𝐵𝑥 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → (𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵}))))
1514pm2.43b 46 . . . . . . . . . . . . . 14 (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → (𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵})))
16153ad2ant2 926 . . . . . . . . . . . . 13 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → (𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵})))
17 eleq2 2101 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → (𝐵𝑥𝐵𝐴))
1817imbi1d 220 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → ((𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐵𝐴𝐵 ∈ (V ∖ {𝐴, 𝐵}))))
19183ad2ant3 927 . . . . . . . . . . . . 13 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → ((𝐵𝑥𝐵 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐵𝐴𝐵 ∈ (V ∖ {𝐴, 𝐵}))))
2016, 19mpbid 135 . . . . . . . . . . . 12 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → (𝐵𝐴𝐵 ∈ (V ∖ {𝐴, 𝐵})))
2110, 20mpd 13 . . . . . . . . . . 11 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐴) → 𝐵 ∈ (V ∖ {𝐴, 𝐵}))
22213expia 1106 . . . . . . . . . 10 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → (𝑥 = 𝐴𝐵 ∈ (V ∖ {𝐴, 𝐵})))
239, 22mtod 589 . . . . . . . . 9 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ 𝑥 = 𝐴)
24 elex 2566 . . . . . . . . . . . . 13 (𝐴𝐵𝐴 ∈ V)
25 prid1g 3474 . . . . . . . . . . . . . 14 (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
26 eldif 2927 . . . . . . . . . . . . . . . 16 (𝐴 ∈ (V ∖ {𝐴, 𝐵}) ↔ (𝐴 ∈ V ∧ ¬ 𝐴 ∈ {𝐴, 𝐵}))
27 pm3.4 316 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ V ∧ ¬ 𝐴 ∈ {𝐴, 𝐵}) → (𝐴 ∈ V → ¬ 𝐴 ∈ {𝐴, 𝐵}))
2826, 27sylbi 114 . . . . . . . . . . . . . . 15 (𝐴 ∈ (V ∖ {𝐴, 𝐵}) → (𝐴 ∈ V → ¬ 𝐴 ∈ {𝐴, 𝐵}))
2928com12 27 . . . . . . . . . . . . . 14 (𝐴 ∈ V → (𝐴 ∈ (V ∖ {𝐴, 𝐵}) → ¬ 𝐴 ∈ {𝐴, 𝐵}))
3025, 29mt2d 555 . . . . . . . . . . . . 13 (𝐴 ∈ V → ¬ 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
3124, 30syl 14 . . . . . . . . . . . 12 (𝐴𝐵 → ¬ 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
3231adantr 261 . . . . . . . . . . 11 ((𝐴𝐵𝐵𝐴) → ¬ 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
3332adantr 261 . . . . . . . . . 10 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
34 simp1l 928 . . . . . . . . . . . 12 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → 𝐴𝐵)
35 eleq1 2100 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
36 eleq1 2100 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴, 𝐵}) ↔ 𝐴 ∈ (V ∖ {𝐴, 𝐵})))
3735, 36imbi12d 223 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → ((𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵}))))
3837spcgv 2640 . . . . . . . . . . . . . . 15 (𝐴𝑥 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵}))))
3938pm2.43b 46 . . . . . . . . . . . . . 14 (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵})))
40393ad2ant2 926 . . . . . . . . . . . . 13 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵})))
41 eleq2 2101 . . . . . . . . . . . . . . 15 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
4241imbi1d 220 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐴𝐵𝐴 ∈ (V ∖ {𝐴, 𝐵}))))
43423ad2ant3 927 . . . . . . . . . . . . 13 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝐴𝐵𝐴 ∈ (V ∖ {𝐴, 𝐵}))))
4440, 43mpbid 135 . . . . . . . . . . . 12 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → (𝐴𝐵𝐴 ∈ (V ∖ {𝐴, 𝐵})))
4534, 44mpd 13 . . . . . . . . . . 11 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) ∧ 𝑥 = 𝐵) → 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
46453expia 1106 . . . . . . . . . 10 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → (𝑥 = 𝐵𝐴 ∈ (V ∖ {𝐴, 𝐵})))
4733, 46mtod 589 . . . . . . . . 9 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ 𝑥 = 𝐵)
48 ioran 669 . . . . . . . . 9 (¬ (𝑥 = 𝐴𝑥 = 𝐵) ↔ (¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵))
4923, 47, 48sylanbrc 394 . . . . . . . 8 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → ¬ (𝑥 = 𝐴𝑥 = 𝐵))
50 vex 2560 . . . . . . . . . 10 𝑥 ∈ V
51 eldif 2927 . . . . . . . . . 10 (𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴, 𝐵}))
5250, 51mpbiran 847 . . . . . . . . 9 (𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ ¬ 𝑥 ∈ {𝐴, 𝐵})
5350elpr 3396 . . . . . . . . 9 (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴𝑥 = 𝐵))
5452, 53xchbinx 607 . . . . . . . 8 (𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ ¬ (𝑥 = 𝐴𝑥 = 𝐵))
5549, 54sylibr 137 . . . . . . 7 (((𝐴𝐵𝐵𝐴) ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵}))) → 𝑥 ∈ (V ∖ {𝐴, 𝐵}))
5655ex 108 . . . . . 6 ((𝐴𝐵𝐵𝐴) → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
5756alrimiv 1754 . . . . 5 ((𝐴𝐵𝐵𝐴) → ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
58 df-ral 2311 . . . . . . . 8 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ ∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵})))
59 clelsb3 2142 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ 𝑦 ∈ (V ∖ {𝐴, 𝐵}))
6059imbi2i 215 . . . . . . . . 9 ((𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵})) ↔ (𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})))
6160albii 1359 . . . . . . . 8 (∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵})) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})))
6258, 61bitri 173 . . . . . . 7 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})))
6362imbi1i 227 . . . . . 6 ((∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})) ↔ (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
6463albii 1359 . . . . 5 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})) ↔ ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴, 𝐵})) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
6557, 64sylibr 137 . . . 4 ((𝐴𝐵𝐵𝐴) → ∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})))
66 ax-setind 4262 . . . 4 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝑥 ∈ (V ∖ {𝐴, 𝐵})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴, 𝐵}))
6765, 66syl 14 . . 3 ((𝐴𝐵𝐵𝐴) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴, 𝐵}))
68 eleq1 2100 . . . . 5 (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴, 𝐵}) ↔ 𝐴 ∈ (V ∖ {𝐴, 𝐵})))
6968spcgv 2640 . . . 4 (𝐴𝐵 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝐴 ∈ (V ∖ {𝐴, 𝐵})))
7069adantr 261 . . 3 ((𝐴𝐵𝐵𝐴) → (∀𝑥 𝑥 ∈ (V ∖ {𝐴, 𝐵}) → 𝐴 ∈ (V ∖ {𝐴, 𝐵})))
7167, 70mpd 13 . 2 ((𝐴𝐵𝐵𝐴) → 𝐴 ∈ (V ∖ {𝐴, 𝐵}))
7271, 32pm2.65i 568 1 ¬ (𝐴𝐵𝐵𝐴)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 629   ∧ w3a 885  ∀wal 1241   = wceq 1243   ∈ wcel 1393  [wsb 1645  ∀wral 2306  Vcvv 2557   ∖ cdif 2914  {cpr 3376 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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-setind 4262 This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-v 2559  df-dif 2920  df-un 2922  df-sn 3381  df-pr 3382 This theorem is referenced by:  preleq  4279  suc11g  4281  ordsuc  4287  2pwuninelg  5898  nntri2  6073  nndcel  6078
 Copyright terms: Public domain W3C validator