Step | Hyp | Ref
| Expression |
1 | | wfrlem10.2 |
. . . 4
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) |
2 | 1 | wfrlem8 7422 |
. . 3
⊢
(Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ ↔ Pred(𝑅, 𝐴, 𝑧) = Pred(𝑅, dom 𝐹, 𝑧)) |
3 | 2 | biimpi 206 |
. 2
⊢
(Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) = Pred(𝑅, dom 𝐹, 𝑧)) |
4 | | predss 5687 |
. . . 4
⊢
Pred(𝑅, dom 𝐹, 𝑧) ⊆ dom 𝐹 |
5 | 4 | a1i 11 |
. . 3
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → Pred(𝑅, dom 𝐹, 𝑧) ⊆ dom 𝐹) |
6 | | simpr 477 |
. . . . . 6
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → 𝑤 ∈ dom 𝐹) |
7 | | eldifn 3733 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹) |
8 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → (𝑤 ∈ dom 𝐹 ↔ 𝑧 ∈ dom 𝐹)) |
9 | 8 | notbid 308 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (¬ 𝑤 ∈ dom 𝐹 ↔ ¬ 𝑧 ∈ dom 𝐹)) |
10 | 7, 9 | syl5ibrcom 237 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (𝑤 = 𝑧 → ¬ 𝑤 ∈ dom 𝐹)) |
11 | 10 | con2d 129 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (𝑤 ∈ dom 𝐹 → ¬ 𝑤 = 𝑧)) |
12 | 11 | imp 445 |
. . . . . . 7
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → ¬ 𝑤 = 𝑧) |
13 | 1 | wfrdmcl 7423 |
. . . . . . . . . 10
⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) |
14 | 13 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) |
15 | | ssel 3597 |
. . . . . . . . . . . 12
⊢
(Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹 → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑤) → 𝑧 ∈ dom 𝐹)) |
16 | 15 | con3d 148 |
. . . . . . . . . . 11
⊢
(Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹 → (¬ 𝑧 ∈ dom 𝐹 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑤))) |
17 | 7, 16 | syl5com 31 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑤))) |
18 | 17 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → (Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑤))) |
19 | 14, 18 | mpd 15 |
. . . . . . . 8
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑤)) |
20 | | eldifi 3732 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴) |
21 | | elpredg 5694 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ dom 𝐹 ∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑤) ↔ 𝑧𝑅𝑤)) |
22 | 21 | ancoms 469 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ dom 𝐹) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑤) ↔ 𝑧𝑅𝑤)) |
23 | 20, 22 | sylan 488 |
. . . . . . . 8
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑤) ↔ 𝑧𝑅𝑤)) |
24 | 19, 23 | mtbid 314 |
. . . . . . 7
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → ¬ 𝑧𝑅𝑤) |
25 | 1 | wfrdmss 7421 |
. . . . . . . . 9
⊢ dom 𝐹 ⊆ 𝐴 |
26 | 25 | sseli 3599 |
. . . . . . . 8
⊢ (𝑤 ∈ dom 𝐹 → 𝑤 ∈ 𝐴) |
27 | | wfrlem10.1 |
. . . . . . . . . 10
⊢ 𝑅 We 𝐴 |
28 | | weso 5105 |
. . . . . . . . . 10
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝑅 Or 𝐴 |
30 | | solin 5058 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)) |
31 | 29, 30 | mpan 706 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)) |
32 | 26, 20, 31 | syl2anr 495 |
. . . . . . 7
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)) |
33 | 12, 24, 32 | ecase23d 1436 |
. . . . . 6
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → 𝑤𝑅𝑧) |
34 | | vex 3203 |
. . . . . . 7
⊢ 𝑧 ∈ V |
35 | | vex 3203 |
. . . . . . . 8
⊢ 𝑤 ∈ V |
36 | 35 | elpred 5693 |
. . . . . . 7
⊢ (𝑧 ∈ V → (𝑤 ∈ Pred(𝑅, dom 𝐹, 𝑧) ↔ (𝑤 ∈ dom 𝐹 ∧ 𝑤𝑅𝑧))) |
37 | 34, 36 | ax-mp 5 |
. . . . . 6
⊢ (𝑤 ∈ Pred(𝑅, dom 𝐹, 𝑧) ↔ (𝑤 ∈ dom 𝐹 ∧ 𝑤𝑅𝑧)) |
38 | 6, 33, 37 | sylanbrc 698 |
. . . . 5
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → 𝑤 ∈ Pred(𝑅, dom 𝐹, 𝑧)) |
39 | 38 | ex 450 |
. . . 4
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (𝑤 ∈ dom 𝐹 → 𝑤 ∈ Pred(𝑅, dom 𝐹, 𝑧))) |
40 | 39 | ssrdv 3609 |
. . 3
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → dom 𝐹 ⊆ Pred(𝑅, dom 𝐹, 𝑧)) |
41 | 5, 40 | eqssd 3620 |
. 2
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → Pred(𝑅, dom 𝐹, 𝑧) = dom 𝐹) |
42 | 3, 41 | sylan9eqr 2678 |
1
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → Pred(𝑅, 𝐴, 𝑧) = dom 𝐹) |