Step | Hyp | Ref
| Expression |
1 | | elex 3430 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | wemapso.t |
. . 3
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
3 | | ssid 3878 |
. . 3
⊢ (𝐵 ↑𝑚
𝐴) ⊆ (𝐵 ↑𝑚
𝐴) |
4 | | simp1 1116 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝐴 ∈ V) |
5 | | weso 5395 |
. . . 4
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
6 | 5 | 3ad2ant2 1114 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑅 Or 𝐴) |
7 | | simp3 1118 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑆 Or 𝐵) |
8 | | simpl1 1171 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝐴 ∈ V) |
9 | | difss 3997 |
. . . . . . 7
⊢ (𝑎 ∖ 𝑏) ⊆ 𝑎 |
10 | | dmss 5618 |
. . . . . . 7
⊢ ((𝑎 ∖ 𝑏) ⊆ 𝑎 → dom (𝑎 ∖ 𝑏) ⊆ dom 𝑎) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
⊢ dom
(𝑎 ∖ 𝑏) ⊆ dom 𝑎 |
12 | | simprll 766 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) |
13 | | elmapi 8224 |
. . . . . . 7
⊢ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) → 𝑎:𝐴⟶𝐵) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎:𝐴⟶𝐵) |
15 | 11, 14 | fssdm 6358 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ⊆ 𝐴) |
16 | 8, 15 | ssexd 5082 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ∈ V) |
17 | | simpl2 1172 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑅 We 𝐴) |
18 | | wefr 5394 |
. . . . 5
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
19 | 17, 18 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑅 Fr 𝐴) |
20 | | simprr 760 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ≠ 𝑏) |
21 | 14 | ffnd 6343 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎 Fn 𝐴) |
22 | | simprlr 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) |
23 | | elmapi 8224 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝐵 ↑𝑚 𝐴) → 𝑏:𝐴⟶𝐵) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑏:𝐴⟶𝐵) |
25 | 24 | ffnd 6343 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑏 Fn 𝐴) |
26 | | fndmdifeq0 6637 |
. . . . . . 7
⊢ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) → (dom (𝑎 ∖ 𝑏) = ∅ ↔ 𝑎 = 𝑏)) |
27 | 21, 25, 26 | syl2anc 576 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → (dom (𝑎 ∖ 𝑏) = ∅ ↔ 𝑎 = 𝑏)) |
28 | 27 | necon3bid 3008 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → (dom (𝑎 ∖ 𝑏) ≠ ∅ ↔ 𝑎 ≠ 𝑏)) |
29 | 20, 28 | mpbird 249 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ≠ ∅) |
30 | | fri 5366 |
. . . 4
⊢ (((dom
(𝑎 ∖ 𝑏) ∈ V ∧ 𝑅 Fr 𝐴) ∧ (dom (𝑎 ∖ 𝑏) ⊆ 𝐴 ∧ dom (𝑎 ∖ 𝑏) ≠ ∅)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) |
31 | 16, 19, 15, 29, 30 | syl22anc 826 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) |
32 | 2, 3, 4, 6, 7, 31 | wemapsolem 8805 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐵 ↑𝑚 𝐴)) |
33 | 1, 32 | syl3an1 1143 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐵 ↑𝑚 𝐴)) |