Step | Hyp | Ref
| Expression |
1 | | elex 3450 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | simpll3 1205 |
. . . . . . 7
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑏 ∈ 𝐴) → 𝑆 Po 𝐵) |
3 | | elmapi 8269 |
. . . . . . . . 9
⊢ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) → 𝑎:𝐴⟶𝐵) |
4 | 3 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) → 𝑎:𝐴⟶𝐵) |
5 | 4 | ffvelrnda 6707 |
. . . . . . 7
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑏 ∈ 𝐴) → (𝑎‘𝑏) ∈ 𝐵) |
6 | | poirr 5365 |
. . . . . . 7
⊢ ((𝑆 Po 𝐵 ∧ (𝑎‘𝑏) ∈ 𝐵) → ¬ (𝑎‘𝑏)𝑆(𝑎‘𝑏)) |
7 | 2, 5, 6 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑏 ∈ 𝐴) → ¬ (𝑎‘𝑏)𝑆(𝑎‘𝑏)) |
8 | 7 | intnanrd 490 |
. . . . 5
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑏 ∈ 𝐴) → ¬ ((𝑎‘𝑏)𝑆(𝑎‘𝑏) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑎‘𝑐) = (𝑎‘𝑐)))) |
9 | 8 | nrexdv 3230 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) → ¬ ∃𝑏 ∈ 𝐴 ((𝑎‘𝑏)𝑆(𝑎‘𝑏) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑎‘𝑐) = (𝑎‘𝑐)))) |
10 | | wemapso.t |
. . . . . 6
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
11 | 10 | wemaplem1 8846 |
. . . . 5
⊢ ((𝑎 ∈ V ∧ 𝑎 ∈ V) → (𝑎𝑇𝑎 ↔ ∃𝑏 ∈ 𝐴 ((𝑎‘𝑏)𝑆(𝑎‘𝑏) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑎‘𝑐) = (𝑎‘𝑐))))) |
12 | 11 | el2v 3439 |
. . . 4
⊢ (𝑎𝑇𝑎 ↔ ∃𝑏 ∈ 𝐴 ((𝑎‘𝑏)𝑆(𝑎‘𝑏) ∧ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑎‘𝑐) = (𝑎‘𝑐)))) |
13 | 9, 12 | sylnibr 330 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) → ¬ 𝑎𝑇𝑎) |
14 | | simpll1 1203 |
. . . . 5
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝐴 ∈ V) |
15 | | simplr1 1206 |
. . . . 5
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) |
16 | | simplr2 1207 |
. . . . 5
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) |
17 | | simplr3 1208 |
. . . . 5
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑐 ∈ (𝐵 ↑𝑚 𝐴)) |
18 | | simpll2 1204 |
. . . . 5
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑅 Or 𝐴) |
19 | | simpll3 1205 |
. . . . 5
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑆 Po 𝐵) |
20 | | simprl 767 |
. . . . 5
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑎𝑇𝑏) |
21 | | simprr 769 |
. . . . 5
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑏𝑇𝑐) |
22 | 10, 14, 15, 16, 17, 18, 19, 20, 21 | wemaplem3 8848 |
. . . 4
⊢ ((((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) ∧ (𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐)) → 𝑎𝑇𝑐) |
23 | 22 | ex 413 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑐 ∈ (𝐵 ↑𝑚 𝐴))) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)) |
24 | 13, 23 | ispod 5362 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑𝑚 𝐴)) |
25 | 1, 24 | syl3an1 1154 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑𝑚 𝐴)) |