Step | Hyp | Ref
| Expression |
1 | | wemapso.t |
. 2
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
2 | | wemapso2.u |
. . 3
⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} |
3 | | ssrab2 3687 |
. . 3
⊢ {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} ⊆ (𝐵 ↑𝑚 𝐴) |
4 | 2, 3 | eqsstri 3635 |
. 2
⊢ 𝑈 ⊆ (𝐵 ↑𝑚 𝐴) |
5 | | elex 3212 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
6 | 5 | 3ad2ant1 1082 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝐴 ∈ V) |
7 | 6 | adantr 481 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝐴 ∈ V) |
8 | | simpl2 1065 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑅 Or 𝐴) |
9 | | simpl3 1066 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑆 Or 𝐵) |
10 | | simprll 802 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝑈) |
11 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (𝑥 finSupp 𝑍 ↔ 𝑎 finSupp 𝑍)) |
12 | 11, 2 | elrab2 3366 |
. . . . . . 7
⊢ (𝑎 ∈ 𝑈 ↔ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑎 finSupp 𝑍)) |
13 | 12 | simprbi 480 |
. . . . . 6
⊢ (𝑎 ∈ 𝑈 → 𝑎 finSupp 𝑍) |
14 | 10, 13 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 finSupp 𝑍) |
15 | | simprlr 803 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝑈) |
16 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → (𝑥 finSupp 𝑍 ↔ 𝑏 finSupp 𝑍)) |
17 | 16, 2 | elrab2 3366 |
. . . . . . 7
⊢ (𝑏 ∈ 𝑈 ↔ (𝑏 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝑏 finSupp 𝑍)) |
18 | 17 | simprbi 480 |
. . . . . 6
⊢ (𝑏 ∈ 𝑈 → 𝑏 finSupp 𝑍) |
19 | 15, 18 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 finSupp 𝑍) |
20 | 14, 19 | fsuppunfi 8295 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ∈ Fin) |
21 | 4, 10 | sseldi 3601 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ (𝐵 ↑𝑚 𝐴)) |
22 | | elmapi 7879 |
. . . . . . . 8
⊢ (𝑎 ∈ (𝐵 ↑𝑚 𝐴) → 𝑎:𝐴⟶𝐵) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎:𝐴⟶𝐵) |
24 | | ffn 6045 |
. . . . . . 7
⊢ (𝑎:𝐴⟶𝐵 → 𝑎 Fn 𝐴) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 Fn 𝐴) |
26 | 4, 15 | sseldi 3601 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ (𝐵 ↑𝑚 𝐴)) |
27 | | elmapi 7879 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝐵 ↑𝑚 𝐴) → 𝑏:𝐴⟶𝐵) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏:𝐴⟶𝐵) |
29 | | ffn 6045 |
. . . . . . 7
⊢ (𝑏:𝐴⟶𝐵 → 𝑏 Fn 𝐴) |
30 | 28, 29 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 Fn 𝐴) |
31 | | fndmdif 6321 |
. . . . . 6
⊢ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) → dom (𝑎 ∖ 𝑏) = {𝑐 ∈ 𝐴 ∣ (𝑎‘𝑐) ≠ (𝑏‘𝑐)}) |
32 | 25, 30, 31 | syl2anc 693 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) = {𝑐 ∈ 𝐴 ∣ (𝑎‘𝑐) ≠ (𝑏‘𝑐)}) |
33 | | eqtr3 2643 |
. . . . . . . . . 10
⊢ (((𝑎‘𝑐) = 𝑍 ∧ (𝑏‘𝑐) = 𝑍) → (𝑎‘𝑐) = (𝑏‘𝑐)) |
34 | 33 | necon3ai 2819 |
. . . . . . . . 9
⊢ ((𝑎‘𝑐) ≠ (𝑏‘𝑐) → ¬ ((𝑎‘𝑐) = 𝑍 ∧ (𝑏‘𝑐) = 𝑍)) |
35 | | neorian 2888 |
. . . . . . . . 9
⊢ (((𝑎‘𝑐) ≠ 𝑍 ∨ (𝑏‘𝑐) ≠ 𝑍) ↔ ¬ ((𝑎‘𝑐) = 𝑍 ∧ (𝑏‘𝑐) = 𝑍)) |
36 | 34, 35 | sylibr 224 |
. . . . . . . 8
⊢ ((𝑎‘𝑐) ≠ (𝑏‘𝑐) → ((𝑎‘𝑐) ≠ 𝑍 ∨ (𝑏‘𝑐) ≠ 𝑍)) |
37 | | elun 3753 |
. . . . . . . . 9
⊢ (𝑐 ∈ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ↔ (𝑐 ∈ (𝑎 supp 𝑍) ∨ 𝑐 ∈ (𝑏 supp 𝑍))) |
38 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎‘𝑐) ∈ V |
39 | | eldifsn 4317 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎‘𝑐) ∈ (V ∖ {𝑍}) ↔ ((𝑎‘𝑐) ∈ V ∧ (𝑎‘𝑐) ≠ 𝑍)) |
40 | 38, 39 | mpbiran 953 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎‘𝑐) ∈ (V ∖ {𝑍}) ↔ (𝑎‘𝑐) ≠ 𝑍) |
41 | 40 | bicomi 214 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘𝑐) ≠ 𝑍 ↔ (𝑎‘𝑐) ∈ (V ∖ {𝑍})) |
42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((𝑎‘𝑐) ≠ 𝑍 ↔ (𝑎‘𝑐) ∈ (V ∖ {𝑍}))) |
43 | 42 | anbi2d 740 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((𝑐 ∈ 𝐴 ∧ (𝑎‘𝑐) ≠ 𝑍) ↔ (𝑐 ∈ 𝐴 ∧ (𝑎‘𝑐) ∈ (V ∖ {𝑍})))) |
44 | 25 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝑎 Fn 𝐴) |
45 | 7 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝐴 ∈ V) |
46 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑍 ∈ 𝑊) |
47 | 46 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝑍 ∈ 𝑊) |
48 | | elsuppfn 7303 |
. . . . . . . . . . . . 13
⊢ ((𝑎 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 𝑍 ∈ 𝑊) → (𝑐 ∈ (𝑎 supp 𝑍) ↔ (𝑐 ∈ 𝐴 ∧ (𝑎‘𝑐) ≠ 𝑍))) |
49 | 44, 45, 47, 48 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ (𝑎 supp 𝑍) ↔ (𝑐 ∈ 𝐴 ∧ (𝑎‘𝑐) ≠ 𝑍))) |
50 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴) |
51 | 50 | biantrurd 529 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((𝑎‘𝑐) ∈ (V ∖ {𝑍}) ↔ (𝑐 ∈ 𝐴 ∧ (𝑎‘𝑐) ∈ (V ∖ {𝑍})))) |
52 | 43, 49, 51 | 3bitr4d 300 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ (𝑎 supp 𝑍) ↔ (𝑎‘𝑐) ∈ (V ∖ {𝑍}))) |
53 | 52, 40 | syl6bb 276 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ (𝑎 supp 𝑍) ↔ (𝑎‘𝑐) ≠ 𝑍)) |
54 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏‘𝑐) ∈ V |
55 | | eldifsn 4317 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏‘𝑐) ∈ (V ∖ {𝑍}) ↔ ((𝑏‘𝑐) ∈ V ∧ (𝑏‘𝑐) ≠ 𝑍)) |
56 | 54, 55 | mpbiran 953 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑐) ∈ (V ∖ {𝑍}) ↔ (𝑏‘𝑐) ≠ 𝑍) |
57 | 56 | bicomi 214 |
. . . . . . . . . . . . . 14
⊢ ((𝑏‘𝑐) ≠ 𝑍 ↔ (𝑏‘𝑐) ∈ (V ∖ {𝑍})) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((𝑏‘𝑐) ≠ 𝑍 ↔ (𝑏‘𝑐) ∈ (V ∖ {𝑍}))) |
59 | 58 | anbi2d 740 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((𝑐 ∈ 𝐴 ∧ (𝑏‘𝑐) ≠ 𝑍) ↔ (𝑐 ∈ 𝐴 ∧ (𝑏‘𝑐) ∈ (V ∖ {𝑍})))) |
60 | 30 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝑏 Fn 𝐴) |
61 | | simpll1 1100 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝐴 ∈ 𝑉) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝐴 ∈ 𝑉) |
63 | | elsuppfn 7303 |
. . . . . . . . . . . . 13
⊢ ((𝑏 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑐 ∈ (𝑏 supp 𝑍) ↔ (𝑐 ∈ 𝐴 ∧ (𝑏‘𝑐) ≠ 𝑍))) |
64 | 60, 62, 47, 63 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ (𝑏 supp 𝑍) ↔ (𝑐 ∈ 𝐴 ∧ (𝑏‘𝑐) ≠ 𝑍))) |
65 | 50 | biantrurd 529 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((𝑏‘𝑐) ∈ (V ∖ {𝑍}) ↔ (𝑐 ∈ 𝐴 ∧ (𝑏‘𝑐) ∈ (V ∖ {𝑍})))) |
66 | 59, 64, 65 | 3bitr4d 300 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ (𝑏 supp 𝑍) ↔ (𝑏‘𝑐) ∈ (V ∖ {𝑍}))) |
67 | 66, 56 | syl6bb 276 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ (𝑏 supp 𝑍) ↔ (𝑏‘𝑐) ≠ 𝑍)) |
68 | 53, 67 | orbi12d 746 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((𝑐 ∈ (𝑎 supp 𝑍) ∨ 𝑐 ∈ (𝑏 supp 𝑍)) ↔ ((𝑎‘𝑐) ≠ 𝑍 ∨ (𝑏‘𝑐) ≠ 𝑍))) |
69 | 37, 68 | syl5bb 272 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ↔ ((𝑎‘𝑐) ≠ 𝑍 ∨ (𝑏‘𝑐) ≠ 𝑍))) |
70 | 36, 69 | syl5ibr 236 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((𝑎‘𝑐) ≠ (𝑏‘𝑐) → 𝑐 ∈ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)))) |
71 | 70 | ralrimiva 2966 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∀𝑐 ∈ 𝐴 ((𝑎‘𝑐) ≠ (𝑏‘𝑐) → 𝑐 ∈ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)))) |
72 | | rabss 3679 |
. . . . . 6
⊢ ({𝑐 ∈ 𝐴 ∣ (𝑎‘𝑐) ≠ (𝑏‘𝑐)} ⊆ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ↔ ∀𝑐 ∈ 𝐴 ((𝑎‘𝑐) ≠ (𝑏‘𝑐) → 𝑐 ∈ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)))) |
73 | 71, 72 | sylibr 224 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → {𝑐 ∈ 𝐴 ∣ (𝑎‘𝑐) ≠ (𝑏‘𝑐)} ⊆ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍))) |
74 | 32, 73 | eqsstrd 3639 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ⊆ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍))) |
75 | | ssfi 8180 |
. . . 4
⊢ ((((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ∈ Fin ∧ dom (𝑎 ∖ 𝑏) ⊆ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍))) → dom (𝑎 ∖ 𝑏) ∈ Fin) |
76 | 20, 74, 75 | syl2anc 693 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ∈ Fin) |
77 | | suppssdm 7308 |
. . . . . . . 8
⊢ (𝑎 supp 𝑍) ⊆ dom 𝑎 |
78 | | fdm 6051 |
. . . . . . . . 9
⊢ (𝑎:𝐴⟶𝐵 → dom 𝑎 = 𝐴) |
79 | 23, 78 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom 𝑎 = 𝐴) |
80 | 77, 79 | syl5sseq 3653 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑎 supp 𝑍) ⊆ 𝐴) |
81 | | suppssdm 7308 |
. . . . . . . 8
⊢ (𝑏 supp 𝑍) ⊆ dom 𝑏 |
82 | | fdm 6051 |
. . . . . . . . 9
⊢ (𝑏:𝐴⟶𝐵 → dom 𝑏 = 𝐴) |
83 | 28, 82 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom 𝑏 = 𝐴) |
84 | 81, 83 | syl5sseq 3653 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑏 supp 𝑍) ⊆ 𝐴) |
85 | 80, 84 | unssd 3789 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ⊆ 𝐴) |
86 | 8 | adantr 481 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑅 Or 𝐴) |
87 | | soss 5053 |
. . . . . 6
⊢ (((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ⊆ 𝐴 → (𝑅 Or 𝐴 → 𝑅 Or ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)))) |
88 | 85, 86, 87 | sylc 65 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑅 Or ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍))) |
89 | | wofi 8209 |
. . . . 5
⊢ ((𝑅 Or ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ∧ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ∈ Fin) → 𝑅 We ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍))) |
90 | 88, 20, 89 | syl2anc 693 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑅 We ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍))) |
91 | | wefr 5104 |
. . . 4
⊢ (𝑅 We ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) → 𝑅 Fr ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍))) |
92 | 90, 91 | syl 17 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑅 Fr ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍))) |
93 | | simprr 796 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ≠ 𝑏) |
94 | | fndmdifeq0 6323 |
. . . . . 6
⊢ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) → (dom (𝑎 ∖ 𝑏) = ∅ ↔ 𝑎 = 𝑏)) |
95 | 25, 30, 94 | syl2anc 693 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (dom (𝑎 ∖ 𝑏) = ∅ ↔ 𝑎 = 𝑏)) |
96 | 95 | necon3bid 2838 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (dom (𝑎 ∖ 𝑏) ≠ ∅ ↔ 𝑎 ≠ 𝑏)) |
97 | 93, 96 | mpbird 247 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) ≠ ∅) |
98 | | fri 5076 |
. . 3
⊢ (((dom
(𝑎 ∖ 𝑏) ∈ Fin ∧ 𝑅 Fr ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍))) ∧ (dom (𝑎 ∖ 𝑏) ⊆ ((𝑎 supp 𝑍) ∪ (𝑏 supp 𝑍)) ∧ dom (𝑎 ∖ 𝑏) ≠ ∅)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) |
99 | 76, 92, 74, 97, 98 | syl22anc 1327 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) |
100 | 1, 4, 7, 8, 9, 99 | wemapsolem 8455 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑇 Or 𝑈) |