Step | Hyp | Ref
| Expression |
1 | | simpllr 776 |
. . . . . 6
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑏 ∈ 𝐴) → 𝑆 Po 𝐵) |
2 | | elmapi 8530 |
. . . . . . . 8
⊢ (𝑎 ∈ (𝐵 ↑m 𝐴) → 𝑎:𝐴⟶𝐵) |
3 | 2 | adantl 485 |
. . . . . . 7
⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑m 𝐴)) → 𝑎:𝐴⟶𝐵) |
4 | 3 | ffvelrnda 6904 |
. . . . . 6
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑏 ∈ 𝐴) → (𝑎‘𝑏) ∈ 𝐵) |
5 | | poirr 5480 |
. . . . . 6
⊢ ((𝑆 Po 𝐵 ∧ (𝑎‘𝑏) ∈ 𝐵) → ¬ (𝑎‘𝑏)𝑆(𝑎‘𝑏)) |
6 | 1, 4, 5 | syl2anc 587 |
. . . . 5
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑏 ∈ 𝐴) → ¬ (𝑎‘𝑏)𝑆(𝑎‘𝑏)) |
7 | 6 | intnanrd 493 |
. . . 4
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑏 ∈ 𝐴) → ¬ ((𝑎‘𝑏)𝑆(𝑎‘𝑏) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑎‘𝑐) = (𝑎‘𝑐)))) |
8 | 7 | nrexdv 3189 |
. . 3
⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑m 𝐴)) → ¬ ∃𝑏 ∈ 𝐴 ((𝑎‘𝑏)𝑆(𝑎‘𝑏) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑎‘𝑐) = (𝑎‘𝑐)))) |
9 | | wemapso.t |
. . . . 5
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
10 | 9 | wemaplem1 9162 |
. . . 4
⊢ ((𝑎 ∈ V ∧ 𝑎 ∈ V) → (𝑎𝑇𝑎 ↔ ∃𝑏 ∈ 𝐴 ((𝑎‘𝑏)𝑆(𝑎‘𝑏) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑎‘𝑐) = (𝑎‘𝑐))))) |
11 | 10 | el2v 3416 |
. . 3
⊢ (𝑎𝑇𝑎 ↔ ∃𝑏 ∈ 𝐴 ((𝑎‘𝑏)𝑆(𝑎‘𝑏) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑎‘𝑐) = (𝑎‘𝑐)))) |
12 | 8, 11 | sylnibr 332 |
. 2
⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑m 𝐴)) → ¬ 𝑎𝑇𝑎) |
13 | | simplr1 1217 |
. . . 4
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴) ∧ 𝑐 ∈ (𝐵 ↑m 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑎 ∈ (𝐵 ↑m 𝐴)) |
14 | | simplr2 1218 |
. . . 4
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴) ∧ 𝑐 ∈ (𝐵 ↑m 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑏 ∈ (𝐵 ↑m 𝐴)) |
15 | | simplr3 1219 |
. . . 4
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴) ∧ 𝑐 ∈ (𝐵 ↑m 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑐 ∈ (𝐵 ↑m 𝐴)) |
16 | | simplll 775 |
. . . 4
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴) ∧ 𝑐 ∈ (𝐵 ↑m 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑅 Or 𝐴) |
17 | | simpllr 776 |
. . . 4
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴) ∧ 𝑐 ∈ (𝐵 ↑m 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑆 Po 𝐵) |
18 | | simprl 771 |
. . . 4
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴) ∧ 𝑐 ∈ (𝐵 ↑m 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑎𝑇𝑏) |
19 | | simprr 773 |
. . . 4
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴) ∧ 𝑐 ∈ (𝐵 ↑m 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑏𝑇𝑐) |
20 | 9, 13, 14, 15, 16, 17, 18, 19 | wemaplem3 9164 |
. . 3
⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴) ∧ 𝑐 ∈ (𝐵 ↑m 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑎𝑇𝑐) |
21 | 20 | ex 416 |
. 2
⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴) ∧ 𝑐 ∈ (𝐵 ↑m 𝐴))) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)) |
22 | 12, 21 | ispod 5477 |
1
⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑m 𝐴)) |