Step | Hyp | Ref
| Expression |
1 | | wemapso.t |
. 2
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
2 | | ssid 3923 |
. 2
⊢ (𝐵 ↑m 𝐴) ⊆ (𝐵 ↑m 𝐴) |
3 | | weso 5542 |
. . 3
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
4 | 3 | adantr 484 |
. 2
⊢ ((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑅 Or 𝐴) |
5 | | simpr 488 |
. 2
⊢ ((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑆 Or 𝐵) |
6 | | vex 3412 |
. . . . . 6
⊢ 𝑎 ∈ V |
7 | 6 | difexi 5221 |
. . . . 5
⊢ (𝑎 ∖ 𝑏) ∈ V |
8 | 7 | dmex 7689 |
. . . 4
⊢ dom
(𝑎 ∖ 𝑏) ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ∈ V) |
10 | | wefr 5541 |
. . . 4
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
11 | 10 | ad2antrr 726 |
. . 3
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑅 Fr 𝐴) |
12 | | difss 4046 |
. . . . 5
⊢ (𝑎 ∖ 𝑏) ⊆ 𝑎 |
13 | | dmss 5771 |
. . . . 5
⊢ ((𝑎 ∖ 𝑏) ⊆ 𝑎 → dom (𝑎 ∖ 𝑏) ⊆ dom 𝑎) |
14 | 12, 13 | ax-mp 5 |
. . . 4
⊢ dom
(𝑎 ∖ 𝑏) ⊆ dom 𝑎 |
15 | | simprll 779 |
. . . . 5
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ (𝐵 ↑m 𝐴)) |
16 | | elmapi 8530 |
. . . . 5
⊢ (𝑎 ∈ (𝐵 ↑m 𝐴) → 𝑎:𝐴⟶𝐵) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎:𝐴⟶𝐵) |
18 | 14, 17 | fssdm 6565 |
. . 3
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ⊆ 𝐴) |
19 | | simprr 773 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ≠ 𝑏) |
20 | 17 | ffnd 6546 |
. . . . . 6
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑎 Fn 𝐴) |
21 | | simprlr 780 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ (𝐵 ↑m 𝐴)) |
22 | | elmapi 8530 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝐵 ↑m 𝐴) → 𝑏:𝐴⟶𝐵) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑏:𝐴⟶𝐵) |
24 | 23 | ffnd 6546 |
. . . . . 6
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → 𝑏 Fn 𝐴) |
25 | | fndmdifeq0 6864 |
. . . . . 6
⊢ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) → (dom (𝑎 ∖ 𝑏) = ∅ ↔ 𝑎 = 𝑏)) |
26 | 20, 24, 25 | syl2anc 587 |
. . . . 5
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → (dom (𝑎 ∖ 𝑏) = ∅ ↔ 𝑎 = 𝑏)) |
27 | 26 | necon3bid 2985 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → (dom (𝑎 ∖ 𝑏) ≠ ∅ ↔ 𝑎 ≠ 𝑏)) |
28 | 19, 27 | mpbird 260 |
. . 3
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ≠ ∅) |
29 | | fri 5512 |
. . 3
⊢ (((dom
(𝑎 ∖ 𝑏) ∈ V ∧ 𝑅 Fr 𝐴) ∧ (dom (𝑎 ∖ 𝑏) ⊆ 𝐴 ∧ dom (𝑎 ∖ 𝑏) ≠ ∅)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) |
30 | 9, 11, 18, 28, 29 | syl22anc 839 |
. 2
⊢ (((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ (𝐵 ↑m 𝐴) ∧ 𝑏 ∈ (𝐵 ↑m 𝐴)) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) |
31 | 1, 2, 4, 5, 30 | wemapsolem 9166 |
1
⊢ ((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐵 ↑m 𝐴)) |