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

Theorem frirrg 4362
Description: A well-founded relation is irreflexive. This is the case where 𝐴 exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
Assertion
Ref Expression
frirrg ((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) → ¬ 𝐵𝑅𝐵)

Proof of Theorem frirrg
Dummy variables 𝑠 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 110 . . . 4 (((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐴 ⊆ (𝐴 ∖ {𝐵})) → 𝐴 ⊆ (𝐴 ∖ {𝐵}))
2 simpl3 1003 . . . 4 (((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐴 ⊆ (𝐴 ∖ {𝐵})) → 𝐵𝐴)
31, 2sseldd 3168 . . 3 (((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐴 ⊆ (𝐴 ∖ {𝐵})) → 𝐵 ∈ (𝐴 ∖ {𝐵}))
4 neldifsnd 3735 . . 3 (((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐴 ⊆ (𝐴 ∖ {𝐵})) → ¬ 𝐵 ∈ (𝐴 ∖ {𝐵}))
53, 4pm2.65da 662 . 2 ((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) → ¬ 𝐴 ⊆ (𝐴 ∖ {𝐵}))
6 simplr 528 . . . . . 6 (((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) → 𝑥𝐴)
7 simplr 528 . . . . . . . . . . 11 ((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) → 𝐵𝑅𝐵)
87ad2antrr 488 . . . . . . . . . 10 ((((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) ∧ 𝑥 = 𝐵) → 𝐵𝑅𝐵)
9 simpr 110 . . . . . . . . . 10 ((((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵)
108, 9breqtrrd 4043 . . . . . . . . 9 ((((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) ∧ 𝑥 = 𝐵) → 𝐵𝑅𝑥)
11 breq1 4018 . . . . . . . . . . 11 (𝑦 = 𝐵 → (𝑦𝑅𝑥𝐵𝑅𝑥))
12 eleq1 2250 . . . . . . . . . . 11 (𝑦 = 𝐵 → (𝑦 ∈ (𝐴 ∖ {𝐵}) ↔ 𝐵 ∈ (𝐴 ∖ {𝐵})))
1311, 12imbi12d 234 . . . . . . . . . 10 (𝑦 = 𝐵 → ((𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) ↔ (𝐵𝑅𝑥𝐵 ∈ (𝐴 ∖ {𝐵}))))
14 simplr 528 . . . . . . . . . 10 ((((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) ∧ 𝑥 = 𝐵) → ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})))
15 simpll3 1039 . . . . . . . . . . 11 ((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) → 𝐵𝐴)
1615ad2antrr 488 . . . . . . . . . 10 ((((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) ∧ 𝑥 = 𝐵) → 𝐵𝐴)
1713, 14, 16rspcdva 2858 . . . . . . . . 9 ((((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) ∧ 𝑥 = 𝐵) → (𝐵𝑅𝑥𝐵 ∈ (𝐴 ∖ {𝐵})))
1810, 17mpd 13 . . . . . . . 8 ((((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) ∧ 𝑥 = 𝐵) → 𝐵 ∈ (𝐴 ∖ {𝐵}))
19 neldifsnd 3735 . . . . . . . 8 ((((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) ∧ 𝑥 = 𝐵) → ¬ 𝐵 ∈ (𝐴 ∖ {𝐵}))
2018, 19pm2.65da 662 . . . . . . 7 (((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) → ¬ 𝑥 = 𝐵)
21 velsn 3621 . . . . . . 7 (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
2220, 21sylnibr 678 . . . . . 6 (((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) → ¬ 𝑥 ∈ {𝐵})
236, 22eldifd 3151 . . . . 5 (((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) ∧ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))) → 𝑥 ∈ (𝐴 ∖ {𝐵}))
2423ex 115 . . . 4 ((((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) ∧ 𝑥𝐴) → (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵})))
2524ralrimiva 2560 . . 3 (((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) → ∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵})))
26 df-frind 4344 . . . . . . . 8 (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)
27 df-frfor 4343 . . . . . . . . 9 ( FrFor 𝑅𝐴𝑠 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠))
2827albii 1480 . . . . . . . 8 (∀𝑠 FrFor 𝑅𝐴𝑠 ↔ ∀𝑠(∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠))
2926, 28bitri 184 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑠(∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠))
3029biimpi 120 . . . . . 6 (𝑅 Fr 𝐴 → ∀𝑠(∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠))
31303ad2ant1 1019 . . . . 5 ((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) → ∀𝑠(∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠))
32 difexg 4156 . . . . . . 7 (𝐴𝑉 → (𝐴 ∖ {𝐵}) ∈ V)
33 eleq2 2251 . . . . . . . . . . . . 13 (𝑠 = (𝐴 ∖ {𝐵}) → (𝑦𝑠𝑦 ∈ (𝐴 ∖ {𝐵})))
3433imbi2d 230 . . . . . . . . . . . 12 (𝑠 = (𝐴 ∖ {𝐵}) → ((𝑦𝑅𝑥𝑦𝑠) ↔ (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))))
3534ralbidv 2487 . . . . . . . . . . 11 (𝑠 = (𝐴 ∖ {𝐵}) → (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) ↔ ∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵}))))
36 eleq2 2251 . . . . . . . . . . 11 (𝑠 = (𝐴 ∖ {𝐵}) → (𝑥𝑠𝑥 ∈ (𝐴 ∖ {𝐵})))
3735, 36imbi12d 234 . . . . . . . . . 10 (𝑠 = (𝐴 ∖ {𝐵}) → ((∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) ↔ (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵}))))
3837ralbidv 2487 . . . . . . . . 9 (𝑠 = (𝐴 ∖ {𝐵}) → (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) ↔ ∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵}))))
39 sseq2 3191 . . . . . . . . 9 (𝑠 = (𝐴 ∖ {𝐵}) → (𝐴𝑠𝐴 ⊆ (𝐴 ∖ {𝐵})))
4038, 39imbi12d 234 . . . . . . . 8 (𝑠 = (𝐴 ∖ {𝐵}) → ((∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠) ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐴 ⊆ (𝐴 ∖ {𝐵}))))
4140spcgv 2836 . . . . . . 7 ((𝐴 ∖ {𝐵}) ∈ V → (∀𝑠(∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠) → (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐴 ⊆ (𝐴 ∖ {𝐵}))))
4232, 41syl 14 . . . . . 6 (𝐴𝑉 → (∀𝑠(∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠) → (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐴 ⊆ (𝐴 ∖ {𝐵}))))
43423ad2ant2 1020 . . . . 5 ((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) → (∀𝑠(∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠) → (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐴 ⊆ (𝐴 ∖ {𝐵}))))
4431, 43mpd 13 . . . 4 ((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) → (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐴 ⊆ (𝐴 ∖ {𝐵})))
4544adantr 276 . . 3 (((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) → (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐴 ⊆ (𝐴 ∖ {𝐵})))
4625, 45mpd 13 . 2 (((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) ∧ 𝐵𝑅𝐵) → 𝐴 ⊆ (𝐴 ∖ {𝐵}))
475, 46mtand 666 1 ((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) → ¬ 𝐵𝑅𝐵)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  w3a 979  wal 1361   = wceq 1363  wcel 2158  wral 2465  Vcvv 2749  cdif 3138  wss 3141  {csn 3604   class class class wbr 4015   FrFor wfrfor 4339   Fr wfr 4340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169  ax-sep 4133
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-v 2751  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-sn 3610  df-pr 3611  df-op 3613  df-br 4016  df-frfor 4343  df-frind 4344
This theorem is referenced by:  efrirr  4365  wepo  4371  wetriext  4588
  Copyright terms: Public domain W3C validator