Step | Hyp | Ref
| Expression |
1 | | wemapwe.u |
. . . . . . . . 9
⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} |
2 | | eqid 2740 |
. . . . . . . . 9
⊢ {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} |
3 | | eqid 2740 |
. . . . . . . . 9
⊢ (◡𝐺‘𝑍) = (◡𝐺‘𝑍) |
4 | | simprr 770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐴 ∈ V) |
5 | | wemapwe.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 We 𝐴) |
6 | 5 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑅 We 𝐴) |
7 | | wemapwe.5 |
. . . . . . . . . . . 12
⊢ 𝐹 = OrdIso(𝑅, 𝐴) |
8 | 7 | oiiso 9274 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴)) |
9 | 4, 6, 8 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴)) |
10 | | isof1o 7190 |
. . . . . . . . . 10
⊢ (𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) → 𝐹:dom 𝐹–1-1-onto→𝐴) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹:dom 𝐹–1-1-onto→𝐴) |
12 | | simprl 768 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ∈ V) |
13 | | wemapwe.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 We 𝐵) |
14 | 13 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑆 We 𝐵) |
15 | | wemapwe.6 |
. . . . . . . . . . . 12
⊢ 𝐺 = OrdIso(𝑆, 𝐵) |
16 | 15 | oiiso 9274 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ V ∧ 𝑆 We 𝐵) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵)) |
17 | 12, 14, 16 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵)) |
18 | | isof1o 7190 |
. . . . . . . . . 10
⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → 𝐺:dom 𝐺–1-1-onto→𝐵) |
19 | | f1ocnv 6726 |
. . . . . . . . . 10
⊢ (𝐺:dom 𝐺–1-1-onto→𝐵 → ◡𝐺:𝐵–1-1-onto→dom
𝐺) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ◡𝐺:𝐵–1-1-onto→dom
𝐺) |
21 | 7 | oiexg 9272 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → 𝐹 ∈ V) |
22 | 21 | ad2antll 726 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐹 ∈ V) |
23 | 22 | dmexd 7746 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ V) |
24 | 15 | oiexg 9272 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → 𝐺 ∈ V) |
25 | 24 | ad2antrl 725 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺 ∈ V) |
26 | 25 | dmexd 7746 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ V) |
27 | | wemapwe.7 |
. . . . . . . . . 10
⊢ 𝑍 = (𝐺‘∅) |
28 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐺:dom 𝐺–1-1-onto→𝐵) |
29 | | f1ofo 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:dom 𝐺–1-1-onto→𝐵 → 𝐺:dom 𝐺–onto→𝐵) |
30 | | forn 6689 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:dom 𝐺–onto→𝐵 → ran 𝐺 = 𝐵) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 = 𝐵) |
32 | | wemapwe.4 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ ∅) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝐵 ≠ ∅) |
34 | 31, 33 | eqnetrd 3013 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ran 𝐺 ≠ ∅) |
35 | | dm0rn0 5833 |
. . . . . . . . . . . . . 14
⊢ (dom
𝐺 = ∅ ↔ ran
𝐺 =
∅) |
36 | 35 | necon3bii 2998 |
. . . . . . . . . . . . 13
⊢ (dom
𝐺 ≠ ∅ ↔ ran
𝐺 ≠
∅) |
37 | 34, 36 | sylibr 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ≠ ∅) |
38 | 15 | oicl 9266 |
. . . . . . . . . . . . 13
⊢ Ord dom
𝐺 |
39 | | ord0eln0 6319 |
. . . . . . . . . . . . 13
⊢ (Ord dom
𝐺 → (∅ ∈
dom 𝐺 ↔ dom 𝐺 ≠ ∅)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (∅
∈ dom 𝐺 ↔ dom
𝐺 ≠
∅) |
41 | 37, 40 | sylibr 233 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ∅ ∈ dom 𝐺) |
42 | 15 | oif 9267 |
. . . . . . . . . . . 12
⊢ 𝐺:dom 𝐺⟶𝐵 |
43 | 42 | ffvelrni 6957 |
. . . . . . . . . . 11
⊢ (∅
∈ dom 𝐺 → (𝐺‘∅) ∈ 𝐵) |
44 | 41, 43 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝐺‘∅) ∈ 𝐵) |
45 | 27, 44 | eqeltrid 2845 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑍 ∈ 𝐵) |
46 | 1, 2, 3, 11, 20, 4, 12, 23, 26, 45 | mapfien 9145 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}) |
47 | | eqid 2740 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅} |
48 | 15 | oion 9273 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ V → dom 𝐺 ∈ On) |
49 | 48 | ad2antrl 725 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐺 ∈ On) |
50 | 7 | oion 9273 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ V → dom 𝐹 ∈ On) |
51 | 50 | ad2antll 726 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom 𝐹 ∈ On) |
52 | 47, 49, 51 | cantnfdm 9400 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅}) |
53 | 27 | fveq2i 6774 |
. . . . . . . . . . . . 13
⊢ (◡𝐺‘𝑍) = (◡𝐺‘(𝐺‘∅)) |
54 | | f1ocnvfv1 7145 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:dom 𝐺–1-1-onto→𝐵 ∧ ∅ ∈ dom 𝐺) → (◡𝐺‘(𝐺‘∅)) = ∅) |
55 | 28, 41, 54 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘(𝐺‘∅)) = ∅) |
56 | 53, 55 | eqtrid 2792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (◡𝐺‘𝑍) = ∅) |
57 | 56 | breq2d 5091 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑥 finSupp (◡𝐺‘𝑍) ↔ 𝑥 finSupp ∅)) |
58 | 57 | rabbidv 3413 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)} = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp ∅}) |
59 | 52, 58 | eqtr4d 2783 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → dom (dom 𝐺 CNF dom 𝐹) = {𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)}) |
60 | 59 | f1oeq3d 6711 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom
(dom 𝐺 CNF dom 𝐹) ↔ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→{𝑥 ∈ (dom 𝐺 ↑m dom 𝐹) ∣ 𝑥 finSupp (◡𝐺‘𝑍)})) |
61 | 46, 60 | mpbird 256 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom
(dom 𝐺 CNF dom 𝐹)) |
62 | | eqid 2740 |
. . . . . . . . 9
⊢ dom (dom
𝐺 CNF dom 𝐹) = dom (dom 𝐺 CNF dom 𝐹) |
63 | | eqid 2740 |
. . . . . . . . 9
⊢
{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} |
64 | 62, 49, 51, 63 | oemapwe 9430 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) ∧ dom OrdIso({〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))}, dom (dom 𝐺 CNF dom 𝐹)) = (dom 𝐺 ↑o dom 𝐹))) |
65 | 64 | simpld 495 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹)) |
66 | | eqid 2740 |
. . . . . . . 8
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} = {〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} |
67 | 66 | f1owe 7220 |
. . . . . . 7
⊢ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))):𝑈–1-1-onto→dom
(dom 𝐺 CNF dom 𝐹) → ({〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} We dom (dom 𝐺 CNF dom 𝐹) → {〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈)) |
68 | 61, 65, 67 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈) |
69 | | weinxp 5672 |
. . . . . 6
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} We 𝑈 ↔ ({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈) |
70 | 68, 69 | sylib 217 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈) |
71 | 11 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹:dom 𝐹–1-1-onto→𝐴) |
72 | | f1ofn 6715 |
. . . . . . . . . . . 12
⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹 Fn dom 𝐹) |
73 | | fveq2 6771 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑐) → (𝑥‘𝑧) = (𝑥‘(𝐹‘𝑐))) |
74 | | fveq2 6771 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑐) → (𝑦‘𝑧) = (𝑦‘(𝐹‘𝑐))) |
75 | 73, 74 | breq12d 5092 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐹‘𝑐) → ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ↔ (𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)))) |
76 | | breq1 5082 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐹‘𝑐) → (𝑧𝑅𝑤 ↔ (𝐹‘𝑐)𝑅𝑤)) |
77 | 76 | imbi1d 342 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑐) → ((𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
78 | 77 | ralbidv 3123 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐹‘𝑐) → (∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
79 | 75, 78 | anbi12d 631 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹‘𝑐) → (((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
80 | 79 | rexrn 6960 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn dom 𝐹 → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
81 | 71, 72, 80 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
82 | | f1ofo 6721 |
. . . . . . . . . . . . 13
⊢ (𝐹:dom 𝐹–1-1-onto→𝐴 → 𝐹:dom 𝐹–onto→𝐴) |
83 | | forn 6689 |
. . . . . . . . . . . . 13
⊢ (𝐹:dom 𝐹–onto→𝐴 → ran 𝐹 = 𝐴) |
84 | 71, 82, 83 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ran 𝐹 = 𝐴) |
85 | 84 | rexeqdv 3348 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ ran 𝐹((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))))) |
86 | 25 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐺 ∈ V) |
87 | | cnvexg 7765 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ V → ◡𝐺 ∈ V) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ◡𝐺 ∈ V) |
89 | | vex 3435 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
90 | 22 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐹 ∈ V) |
91 | | coexg 7770 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ V ∧ 𝐹 ∈ V) → (𝑥 ∘ 𝐹) ∈ V) |
92 | 89, 90, 91 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑥 ∘ 𝐹) ∈ V) |
93 | | coexg 7770 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐺 ∈ V ∧ (𝑥 ∘ 𝐹) ∈ V) → (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V) |
94 | 88, 92, 93 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V) |
95 | | vex 3435 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
96 | | coexg 7770 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ V ∧ 𝐹 ∈ V) → (𝑦 ∘ 𝐹) ∈ V) |
97 | 95, 90, 96 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑦 ∘ 𝐹) ∈ V) |
98 | | coexg 7770 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐺 ∈ V ∧ (𝑦 ∘ 𝐹) ∈ V) → (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) |
99 | 88, 97, 98 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) |
100 | | fveq1 6770 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐)) |
101 | | fveq1 6770 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)) |
102 | | eleq12 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎‘𝑐) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∧ (𝑏‘𝑐) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐)) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐))) |
103 | 100, 101,
102 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐))) |
104 | | fveq1 6770 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) → (𝑎‘𝑑) = ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑)) |
105 | | fveq1 6770 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹)) → (𝑏‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) |
106 | 104, 105 | eqeqan12d 2754 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑎‘𝑑) = (𝑏‘𝑑) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))) |
107 | 106 | imbi2d 341 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → ((𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ (𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))) |
108 | 107 | ralbidv 3123 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))) |
109 | 103, 108 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))) |
110 | 109 | rexbidv 3228 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∧ 𝑏 = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) → (∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))) |
111 | 110, 63 | brabga 5450 |
. . . . . . . . . . . . 13
⊢ (((◡𝐺 ∘ (𝑥 ∘ 𝐹)) ∈ V ∧ (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ∈ V) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))) |
112 | 94, 99, 111 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹)){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))) |
113 | | eqid 2740 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))) = (𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹))) |
114 | | coeq1 5765 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑥 → (𝑓 ∘ 𝐹) = (𝑥 ∘ 𝐹)) |
115 | 114 | coeq2d 5770 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑥 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑥 ∘ 𝐹))) |
116 | | simprl 768 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈) |
117 | 113, 115,
116, 94 | fvmptd3 6895 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥) = (◡𝐺 ∘ (𝑥 ∘ 𝐹))) |
118 | | coeq1 5765 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑦 → (𝑓 ∘ 𝐹) = (𝑦 ∘ 𝐹)) |
119 | 118 | coeq2d 5770 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑦 → (◡𝐺 ∘ (𝑓 ∘ 𝐹)) = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) |
120 | | simprr 770 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
121 | 113, 119,
120, 99 | fvmptd3 6895 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) = (◡𝐺 ∘ (𝑦 ∘ 𝐹))) |
122 | 117, 121 | breq12d 5092 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ↔ (◡𝐺 ∘ (𝑥 ∘ 𝐹)){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} (◡𝐺 ∘ (𝑦 ∘ 𝐹)))) |
123 | 17 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵)) |
124 | | isocnv 7197 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 Isom E , 𝑆 (dom 𝐺, 𝐵) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺)) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺)) |
126 | 1 | ssrab3 4020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴) |
127 | 126, 116 | sselid 3924 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ (𝐵 ↑m 𝐴)) |
128 | | elmapi 8620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐵 ↑m 𝐴) → 𝑥:𝐴⟶𝐵) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥:𝐴⟶𝐵) |
130 | 7 | oif 9267 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐹:dom 𝐹⟶𝐴 |
131 | 130 | ffvelrni 6957 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ dom 𝐹 → (𝐹‘𝑐) ∈ 𝐴) |
132 | | ffvelrn 6956 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵) |
133 | 129, 131,
132 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥‘(𝐹‘𝑐)) ∈ 𝐵) |
134 | 126, 120 | sselid 3924 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ (𝐵 ↑m 𝐴)) |
135 | | elmapi 8620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝐵 ↑m 𝐴) → 𝑦:𝐴⟶𝐵) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦:𝐴⟶𝐵) |
137 | | ffvelrn 6956 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦:𝐴⟶𝐵 ∧ (𝐹‘𝑐) ∈ 𝐴) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵) |
138 | 136, 131,
137 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦‘(𝐹‘𝑐)) ∈ 𝐵) |
139 | | isorel 7193 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐺 Isom 𝑆, E (𝐵, dom 𝐺) ∧ ((𝑥‘(𝐹‘𝑐)) ∈ 𝐵 ∧ (𝑦‘(𝐹‘𝑐)) ∈ 𝐵)) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐))))) |
140 | 125, 133,
138, 139 | syl12anc 834 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐))))) |
141 | | fvex 6784 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ∈ V |
142 | 141 | epeli 5498 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐺‘(𝑥‘(𝐹‘𝑐))) E (◡𝐺‘(𝑦‘(𝐹‘𝑐))) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐)))) |
143 | 140, 142 | bitrdi 287 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐))))) |
144 | 129 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑥:𝐴⟶𝐵) |
145 | | fco 6622 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵) |
146 | 144, 130,
145 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵) |
147 | | fvco3 6864 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐))) |
148 | 146, 147 | sylancom 588 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐))) |
149 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑐 ∈ dom 𝐹) |
150 | | fvco3 6864 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐))) |
151 | 130, 149,
150 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑐) = (𝑥‘(𝐹‘𝑐))) |
152 | 151 | fveq2d 6775 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑥‘(𝐹‘𝑐)))) |
153 | 148, 152 | eqtrd 2780 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑥‘(𝐹‘𝑐)))) |
154 | 136 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → 𝑦:𝐴⟶𝐵) |
155 | | fco 6622 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦:𝐴⟶𝐵 ∧ 𝐹:dom 𝐹⟶𝐴) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵) |
156 | 154, 130,
155 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵) |
157 | | fvco3 6864 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∘ 𝐹):dom 𝐹⟶𝐵 ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐))) |
158 | 156, 157 | sylancom 588 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐))) |
159 | | fvco3 6864 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐))) |
160 | 130, 149,
159 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑐) = (𝑦‘(𝐹‘𝑐))) |
161 | 160 | fveq2d 6775 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑐)) = (◡𝐺‘(𝑦‘(𝐹‘𝑐)))) |
162 | 158, 161 | eqtrd 2780 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) = (◡𝐺‘(𝑦‘(𝐹‘𝑐)))) |
163 | 153, 162 | eleq12d 2835 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ↔ (◡𝐺‘(𝑥‘(𝐹‘𝑐))) ∈ (◡𝐺‘(𝑦‘(𝐹‘𝑐))))) |
164 | 143, 163 | bitr4d 281 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → ((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ↔ ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐))) |
165 | 84 | raleqdv 3347 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))) |
166 | | breq2 5083 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝐹‘𝑑) → ((𝐹‘𝑐)𝑅𝑤 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑))) |
167 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = (𝐹‘𝑑) → (𝑥‘𝑤) = (𝑥‘(𝐹‘𝑑))) |
168 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = (𝐹‘𝑑) → (𝑦‘𝑤) = (𝑦‘(𝐹‘𝑑))) |
169 | 167, 168 | eqeq12d 2756 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝐹‘𝑑) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))) |
170 | 166, 169 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = (𝐹‘𝑑) → (((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))) |
171 | 170 | ralrn 6961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 Fn dom 𝐹 → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))) |
172 | 71, 72, 171 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ ran 𝐹((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))) |
173 | 165, 172 | bitr3d 280 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))) |
174 | 173 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))) |
175 | | epel 5499 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 E 𝑑 ↔ 𝑐 ∈ 𝑑) |
176 | 9 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴)) |
177 | | isorel 7193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑))) |
178 | 176, 177 | sylancom 588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 E 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑))) |
179 | 175, 178 | bitr3id 285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑐 ∈ 𝑑 ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑑))) |
180 | 146 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑥 ∘ 𝐹):dom 𝐹⟶𝐵) |
181 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝑑 ∈ dom 𝐹) |
182 | 180, 181 | fvco3d 6865 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑))) |
183 | 156 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (𝑦 ∘ 𝐹):dom 𝐹⟶𝐵) |
184 | 183, 181 | fvco3d 6865 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑))) |
185 | 182, 184 | eqeq12d 2756 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)))) |
186 | 28 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → 𝐺:dom 𝐺–1-1-onto→𝐵) |
187 | | f1of1 6713 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝐺:𝐵–1-1-onto→dom
𝐺 → ◡𝐺:𝐵–1-1→dom 𝐺) |
188 | 186, 19, 187 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ◡𝐺:𝐵–1-1→dom 𝐺) |
189 | 180, 181 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵) |
190 | 183, 181 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵) |
191 | | f1fveq 7132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡𝐺:𝐵–1-1→dom 𝐺 ∧ (((𝑥 ∘ 𝐹)‘𝑑) ∈ 𝐵 ∧ ((𝑦 ∘ 𝐹)‘𝑑) ∈ 𝐵)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑))) |
192 | 188, 189,
190, 191 | syl12anc 834 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((◡𝐺‘((𝑥 ∘ 𝐹)‘𝑑)) = (◡𝐺‘((𝑦 ∘ 𝐹)‘𝑑)) ↔ ((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑))) |
193 | | fvco3 6864 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑))) |
194 | 130, 181,
193 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑥 ∘ 𝐹)‘𝑑) = (𝑥‘(𝐹‘𝑑))) |
195 | | fvco3 6864 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ 𝑑 ∈ dom 𝐹) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑))) |
196 | 130, 181,
195 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑦 ∘ 𝐹)‘𝑑) = (𝑦‘(𝐹‘𝑑))) |
197 | 194, 196 | eqeq12d 2756 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((𝑥 ∘ 𝐹)‘𝑑) = ((𝑦 ∘ 𝐹)‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))) |
198 | 185, 192,
197 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑) ↔ (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑)))) |
199 | 179, 198 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑐 ∈ dom 𝐹 ∧ 𝑑 ∈ dom 𝐹)) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))) |
200 | 199 | anassrs 468 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) ∧ 𝑑 ∈ dom 𝐹) → ((𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))) |
201 | 200 | ralbidva 3122 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)) ↔ ∀𝑑 ∈ dom 𝐹((𝐹‘𝑐)𝑅(𝐹‘𝑑) → (𝑥‘(𝐹‘𝑑)) = (𝑦‘(𝐹‘𝑑))))) |
202 | 174, 201 | bitr4d 281 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑)))) |
203 | 164, 202 | anbi12d 631 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ 𝑐 ∈ dom 𝐹) → (((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ (((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))) |
204 | 203 | rexbidva 3227 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑐 ∈ dom 𝐹(((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑐) ∈ ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → ((◡𝐺 ∘ (𝑥 ∘ 𝐹))‘𝑑) = ((◡𝐺 ∘ (𝑦 ∘ 𝐹))‘𝑑))))) |
205 | 112, 122,
204 | 3bitr4rd 312 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑐 ∈ dom 𝐹((𝑥‘(𝐹‘𝑐))𝑆(𝑦‘(𝐹‘𝑐)) ∧ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑐)𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦))) |
206 | 81, 85, 205 | 3bitr3d 309 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦))) |
207 | 206 | ex 413 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)))) |
208 | 207 | pm5.32rd 578 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ↔ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)))) |
209 | 208 | opabbidv 5145 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → {〈𝑥, 𝑦〉 ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} = {〈𝑥, 𝑦〉 ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))}) |
210 | | wemapwe.t |
. . . . . . . . 9
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
211 | | df-xp 5596 |
. . . . . . . . 9
⊢ (𝑈 × 𝑈) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)} |
212 | 210, 211 | ineq12i 4150 |
. . . . . . . 8
⊢ (𝑇 ∩ (𝑈 × 𝑈)) = ({〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) |
213 | | inopab 5738 |
. . . . . . . 8
⊢
({〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ∩ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {〈𝑥, 𝑦〉 ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} |
214 | 212, 213 | eqtri 2768 |
. . . . . . 7
⊢ (𝑇 ∩ (𝑈 × 𝑈)) = {〈𝑥, 𝑦〉 ∣ (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} |
215 | 211 | ineq2i 4149 |
. . . . . . . 8
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = ({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) |
216 | | inopab 5738 |
. . . . . . . 8
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)}) = {〈𝑥, 𝑦〉 ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} |
217 | 215, 216 | eqtri 2768 |
. . . . . . 7
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) = {〈𝑥, 𝑦〉 ∣ (((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))} |
218 | 209, 214,
217 | 3eqtr4g 2805 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) = ({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈))) |
219 | | weeq1 5578 |
. . . . . 6
⊢ ((𝑇 ∩ (𝑈 × 𝑈)) = ({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)) |
220 | 218, 219 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → ((𝑇 ∩ (𝑈 × 𝑈)) We 𝑈 ↔ ({〈𝑥, 𝑦〉 ∣ ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑥){〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ dom 𝐹((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑑 ∈ dom 𝐹(𝑐 ∈ 𝑑 → (𝑎‘𝑑) = (𝑏‘𝑑)))} ((𝑓 ∈ 𝑈 ↦ (◡𝐺 ∘ (𝑓 ∘ 𝐹)))‘𝑦)} ∩ (𝑈 × 𝑈)) We 𝑈)) |
221 | 70, 220 | mpbird 256 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈) |
222 | | weinxp 5672 |
. . . 4
⊢ (𝑇 We 𝑈 ↔ (𝑇 ∩ (𝑈 × 𝑈)) We 𝑈) |
223 | 221, 222 | sylibr 233 |
. . 3
⊢ ((𝜑 ∧ (𝐵 ∈ V ∧ 𝐴 ∈ V)) → 𝑇 We 𝑈) |
224 | 223 | ex 413 |
. 2
⊢ (𝜑 → ((𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈)) |
225 | | we0 5585 |
. . 3
⊢ 𝑇 We ∅ |
226 | | elmapex 8619 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ↑m 𝐴) → (𝐵 ∈ V ∧ 𝐴 ∈ V)) |
227 | 226 | con3i 154 |
. . . . . . . 8
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → ¬ 𝑥 ∈ (𝐵 ↑m 𝐴)) |
228 | 227 | pm2.21d 121 |
. . . . . . 7
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐵 ↑m 𝐴) → ¬ 𝑥 finSupp 𝑍)) |
229 | 228 | ralrimiv 3109 |
. . . . . 6
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → ∀𝑥 ∈ (𝐵 ↑m 𝐴) ¬ 𝑥 finSupp 𝑍) |
230 | | rabeq0 4324 |
. . . . . 6
⊢ ({𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅ ↔ ∀𝑥 ∈ (𝐵 ↑m 𝐴) ¬ 𝑥 finSupp 𝑍) |
231 | 229, 230 | sylibr 233 |
. . . . 5
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} = ∅) |
232 | 1, 231 | eqtrid 2792 |
. . . 4
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑈 = ∅) |
233 | | weeq2 5579 |
. . . 4
⊢ (𝑈 = ∅ → (𝑇 We 𝑈 ↔ 𝑇 We ∅)) |
234 | 232, 233 | syl 17 |
. . 3
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝑇 We 𝑈 ↔ 𝑇 We ∅)) |
235 | 225, 234 | mpbiri 257 |
. 2
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ∈ V) → 𝑇 We 𝑈) |
236 | 224, 235 | pm2.61d1 180 |
1
⊢ (𝜑 → 𝑇 We 𝑈) |