Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | wemapso.t |
. . 3
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
3 | | ssid 3587 |
. . 3
⊢ (𝐵 ↑𝑚
𝐴) ⊆ (𝐵 ↑𝑚
𝐴) |
4 | | simp1 1054 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝐴 ∈ V) |
5 | | weso 5029 |
. . . 4
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
6 | 5 | 3ad2ant2 1076 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑅 Or 𝐴) |
7 | | simp3 1056 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑆 Or 𝐵) |
8 | | simpl1 1057 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝐴 ∈ V) |
9 | | difss 3699 |
. . . . . . 7
⊢ (𝑎 ∖ 𝑏) ⊆ 𝑎 |
10 | | dmss 5245 |
. . . . . . 7
⊢ ((𝑎 ∖ 𝑏) ⊆ 𝑎 → dom (𝑎 ∖ 𝑏) ⊆ dom 𝑎) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
⊢ dom
(𝑎 ∖ 𝑏) ⊆ dom 𝑎 |
12 | | simprll 798 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) |
13 | | elmapi 7765 |
. . . . . . . . 9
⊢ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) → 𝑎:𝐴⟶𝐵) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎:𝐴⟶𝐵) |
15 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑎:𝐴⟶𝐵 → 𝑎 Fn 𝐴) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎 Fn 𝐴) |
17 | | fndm 5904 |
. . . . . . 7
⊢ (𝑎 Fn 𝐴 → dom 𝑎 = 𝐴) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom 𝑎 = 𝐴) |
19 | 11, 18 | syl5sseq 3616 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ⊆ 𝐴) |
20 | 8, 19 | ssexd 4733 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ∈ V) |
21 | | simpl2 1058 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑅 We 𝐴) |
22 | | wefr 5028 |
. . . . 5
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑅 Fr 𝐴) |
24 | | simprr 792 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ≠ 𝑏) |
25 | | simprlr 799 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) |
26 | | elmapi 7765 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝐵 ↑𝑚 𝐴) → 𝑏:𝐴⟶𝐵) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑏:𝐴⟶𝐵) |
28 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑏:𝐴⟶𝐵 → 𝑏 Fn 𝐴) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑏 Fn 𝐴) |
30 | | fndmdifeq0 6231 |
. . . . . . 7
⊢ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) → (dom (𝑎 ∖ 𝑏) = ∅ ↔ 𝑎 = 𝑏)) |
31 | 16, 29, 30 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → (dom (𝑎 ∖ 𝑏) = ∅ ↔ 𝑎 = 𝑏)) |
32 | 31 | necon3bid 2826 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → (dom (𝑎 ∖ 𝑏) ≠ ∅ ↔ 𝑎 ≠ 𝑏)) |
33 | 24, 32 | mpbird 246 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ≠ ∅) |
34 | | fri 5000 |
. . . 4
⊢ (((dom
(𝑎 ∖ 𝑏) ∈ V ∧ 𝑅 Fr 𝐴) ∧ (dom (𝑎 ∖ 𝑏) ⊆ 𝐴 ∧ dom (𝑎 ∖ 𝑏) ≠ ∅)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) |
35 | 20, 23, 19, 33, 34 | syl22anc 1319 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) |
36 | 2, 3, 4, 6, 7, 35 | wemapsolem 8338 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐵 ↑𝑚 𝐴)) |
37 | 1, 36 | syl3an1 1351 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐵 ↑𝑚 𝐴)) |