Proof of Theorem wsuclemOLD
Step | Hyp | Ref
| Expression |
1 | | wsuclem.1 |
. . 3
⊢ (𝜑 → 𝑅 We 𝐴) |
2 | | wsuclem.2 |
. . 3
⊢ (𝜑 → 𝑅 Se 𝐴) |
3 | | predss 5687 |
. . . 4
⊢
Pred(◡𝑅, 𝐴, 𝑋) ⊆ 𝐴 |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → Pred(◡𝑅, 𝐴, 𝑋) ⊆ 𝐴) |
5 | | wsuclem.3 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
6 | | dfpred3g 5691 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → Pred(◡𝑅, 𝐴, 𝑋) = {𝑤 ∈ 𝐴 ∣ 𝑤◡𝑅𝑋}) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → Pred(◡𝑅, 𝐴, 𝑋) = {𝑤 ∈ 𝐴 ∣ 𝑤◡𝑅𝑋}) |
8 | | elex 3212 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ V) |
9 | 5, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ V) |
10 | | wsuclem.4 |
. . . . 5
⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤) |
11 | | rabn0 3958 |
. . . . . . 7
⊢ ({𝑤 ∈ 𝐴 ∣ 𝑤◡𝑅𝑋} ≠ ∅ ↔ ∃𝑤 ∈ 𝐴 𝑤◡𝑅𝑋) |
12 | | brcnvg 5303 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑋 ∈ V) → (𝑤◡𝑅𝑋 ↔ 𝑋𝑅𝑤)) |
13 | 12 | ancoms 469 |
. . . . . . . 8
⊢ ((𝑋 ∈ V ∧ 𝑤 ∈ 𝐴) → (𝑤◡𝑅𝑋 ↔ 𝑋𝑅𝑤)) |
14 | 13 | rexbidva 3049 |
. . . . . . 7
⊢ (𝑋 ∈ V → (∃𝑤 ∈ 𝐴 𝑤◡𝑅𝑋 ↔ ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤)) |
15 | 11, 14 | syl5bb 272 |
. . . . . 6
⊢ (𝑋 ∈ V → ({𝑤 ∈ 𝐴 ∣ 𝑤◡𝑅𝑋} ≠ ∅ ↔ ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤)) |
16 | 15 | biimpar 502 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤) → {𝑤 ∈ 𝐴 ∣ 𝑤◡𝑅𝑋} ≠ ∅) |
17 | 9, 10, 16 | syl2anc 693 |
. . . 4
⊢ (𝜑 → {𝑤 ∈ 𝐴 ∣ 𝑤◡𝑅𝑋} ≠ ∅) |
18 | 7, 17 | eqnetrd 2861 |
. . 3
⊢ (𝜑 → Pred(◡𝑅, 𝐴, 𝑋) ≠ ∅) |
19 | | tz6.26 5711 |
. . 3
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (Pred(◡𝑅, 𝐴, 𝑋) ⊆ 𝐴 ∧ Pred(◡𝑅, 𝐴, 𝑋) ≠ ∅)) → ∃𝑥 ∈ Pred (◡𝑅, 𝐴, 𝑋)Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) |
20 | 1, 2, 4, 18, 19 | syl22anc 1327 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ Pred (◡𝑅, 𝐴, 𝑋)Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) |
21 | | dfpred3g 5691 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → Pred(◡𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦◡𝑅𝑋}) |
22 | 5, 21 | syl 17 |
. . . 4
⊢ (𝜑 → Pred(◡𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦◡𝑅𝑋}) |
23 | 22 | rexeqdv 3145 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ Pred (◡𝑅, 𝐴, 𝑋)Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ ↔ ∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝑦◡𝑅𝑋}Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅)) |
24 | | breq1 4656 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑦◡𝑅𝑋 ↔ 𝑥◡𝑅𝑋)) |
25 | 24 | rexrab 3370 |
. . . 4
⊢
(∃𝑥 ∈
{𝑦 ∈ 𝐴 ∣ 𝑦◡𝑅𝑋}Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐴 (𝑥◡𝑅𝑋 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅)) |
26 | | noel 3919 |
. . . . . . . . . . . . 13
⊢ ¬
𝑦 ∈
∅ |
27 | | simp2r 1088 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) |
28 | 27 | eleq2d 2687 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → (𝑦 ∈ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) ↔ 𝑦 ∈ ∅)) |
29 | 26, 28 | mtbiri 317 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → ¬ 𝑦 ∈ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥)) |
30 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
31 | 30 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → 𝑥 ∈ V) |
32 | | simp3 1063 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) |
33 | | elpredg 5694 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → (𝑦 ∈ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) ↔ 𝑦𝑅𝑥)) |
34 | 31, 32, 33 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → (𝑦 ∈ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) ↔ 𝑦𝑅𝑥)) |
35 | 29, 34 | mtbid 314 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → ¬ 𝑦𝑅𝑥) |
36 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
37 | 30, 36 | brcnv 5305 |
. . . . . . . . . . 11
⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥) |
38 | 35, 37 | sylnibr 319 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → ¬ 𝑥◡𝑅𝑦) |
39 | 38 | 3expa 1265 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅)) ∧ 𝑦 ∈ Pred(◡𝑅, 𝐴, 𝑋)) → ¬ 𝑥◡𝑅𝑦) |
40 | 39 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅)) → ∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑥◡𝑅𝑦) |
41 | 40 | expr 643 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ → ∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑥◡𝑅𝑦)) |
42 | | simp1rl 1126 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦◡𝑅𝑥) → 𝑥 ∈ 𝐴) |
43 | | simp1rr 1127 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦◡𝑅𝑥) → 𝑥◡𝑅𝑋) |
44 | | simp1l 1085 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦◡𝑅𝑥) → 𝜑) |
45 | 44, 5 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦◡𝑅𝑥) → 𝑋 ∈ 𝑉) |
46 | 30 | elpred 5693 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑉 → (𝑥 ∈ Pred(◡𝑅, 𝐴, 𝑋) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋))) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦◡𝑅𝑥) → (𝑥 ∈ Pred(◡𝑅, 𝐴, 𝑋) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋))) |
48 | 42, 43, 47 | mpbir2and 957 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦◡𝑅𝑥) → 𝑥 ∈ Pred(◡𝑅, 𝐴, 𝑋)) |
49 | | simp3 1063 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦◡𝑅𝑥) → 𝑦◡𝑅𝑥) |
50 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → (𝑦◡𝑅𝑧 ↔ 𝑦◡𝑅𝑥)) |
51 | 50 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Pred(◡𝑅, 𝐴, 𝑋) ∧ 𝑦◡𝑅𝑥) → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧) |
52 | 48, 49, 51 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦◡𝑅𝑥) → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧) |
53 | 52 | 3expia 1267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴) → (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧)) |
54 | 53 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥◡𝑅𝑋)) → ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧)) |
55 | 54 | expr 643 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥◡𝑅𝑋 → ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧))) |
56 | 41, 55 | anim12d 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ ∧ 𝑥◡𝑅𝑋) → (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧)))) |
57 | 56 | ancomsd 470 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥◡𝑅𝑋 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) → (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧)))) |
58 | 57 | reximdva 3017 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ 𝐴 (𝑥◡𝑅𝑋 ∧ Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧)))) |
59 | 25, 58 | syl5bi 232 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝑦◡𝑅𝑋}Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧)))) |
60 | 23, 59 | sylbid 230 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ Pred (◡𝑅, 𝐴, 𝑋)Pred(𝑅, Pred(◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧)))) |
61 | 20, 60 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧))) |