Proof of Theorem fpwwe2lem9
Step | Hyp | Ref
| Expression |
1 | | fpwwe2lem9.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋𝑊𝑅) |
2 | | fpwwe2.1 |
. . . . . . . . . . 11
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
3 | 2 | relopabi 5167 |
. . . . . . . . . 10
⊢ Rel 𝑊 |
4 | 3 | brrelexi 5082 |
. . . . . . . . 9
⊢ (𝑋𝑊𝑅 → 𝑋 ∈ V) |
5 | 1, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ V) |
6 | | fpwwe2.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ V) |
7 | 2, 6 | fpwwe2lem2 9333 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
8 | 1, 7 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) |
9 | 8 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)) |
10 | 9 | simpld 474 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 We 𝑋) |
11 | | fpwwe2lem9.m |
. . . . . . . . 9
⊢ 𝑀 = OrdIso(𝑅, 𝑋) |
12 | 11 | oiiso 8325 |
. . . . . . . 8
⊢ ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
13 | 5, 10, 12 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
14 | | isof1o 6473 |
. . . . . . 7
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀–1-1-onto→𝑋) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀:dom 𝑀–1-1-onto→𝑋) |
16 | | f1ofo 6057 |
. . . . . 6
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → 𝑀:dom 𝑀–onto→𝑋) |
17 | | forn 6031 |
. . . . . 6
⊢ (𝑀:dom 𝑀–onto→𝑋 → ran 𝑀 = 𝑋) |
18 | 15, 16, 17 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝑀 = 𝑋) |
19 | | fpwwe2.3 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
20 | | fpwwe2lem9.y |
. . . . . . 7
⊢ (𝜑 → 𝑌𝑊𝑆) |
21 | | fpwwe2lem9.n |
. . . . . . 7
⊢ 𝑁 = OrdIso(𝑆, 𝑌) |
22 | | fpwwe2lem9.s |
. . . . . . 7
⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) |
23 | 2, 6, 19, 1, 20, 11, 21, 22 | fpwwe2lem8 9338 |
. . . . . 6
⊢ (𝜑 → 𝑀 = (𝑁 ↾ dom 𝑀)) |
24 | 23 | rneqd 5274 |
. . . . 5
⊢ (𝜑 → ran 𝑀 = ran (𝑁 ↾ dom 𝑀)) |
25 | 18, 24 | eqtr3d 2646 |
. . . 4
⊢ (𝜑 → 𝑋 = ran (𝑁 ↾ dom 𝑀)) |
26 | | df-ima 5051 |
. . . 4
⊢ (𝑁 “ dom 𝑀) = ran (𝑁 ↾ dom 𝑀) |
27 | 25, 26 | syl6eqr 2662 |
. . 3
⊢ (𝜑 → 𝑋 = (𝑁 “ dom 𝑀)) |
28 | | imassrn 5396 |
. . . 4
⊢ (𝑁 “ dom 𝑀) ⊆ ran 𝑁 |
29 | 3 | brrelexi 5082 |
. . . . . . . 8
⊢ (𝑌𝑊𝑆 → 𝑌 ∈ V) |
30 | 20, 29 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ V) |
31 | 2, 6 | fpwwe2lem2 9333 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
32 | 20, 31 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))) |
33 | 32 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)) |
34 | 33 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → 𝑆 We 𝑌) |
35 | 21 | oiiso 8325 |
. . . . . . 7
⊢ ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
36 | 30, 34, 35 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
37 | | isof1o 6473 |
. . . . . 6
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁–1-1-onto→𝑌) |
38 | 36, 37 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁:dom 𝑁–1-1-onto→𝑌) |
39 | | f1ofo 6057 |
. . . . 5
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → 𝑁:dom 𝑁–onto→𝑌) |
40 | | forn 6031 |
. . . . 5
⊢ (𝑁:dom 𝑁–onto→𝑌 → ran 𝑁 = 𝑌) |
41 | 38, 39, 40 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran 𝑁 = 𝑌) |
42 | 28, 41 | syl5sseq 3616 |
. . 3
⊢ (𝜑 → (𝑁 “ dom 𝑀) ⊆ 𝑌) |
43 | 27, 42 | eqsstrd 3602 |
. 2
⊢ (𝜑 → 𝑋 ⊆ 𝑌) |
44 | 8 | simpld 474 |
. . . . . 6
⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋))) |
45 | 44 | simprd 478 |
. . . . 5
⊢ (𝜑 → 𝑅 ⊆ (𝑋 × 𝑋)) |
46 | | relxp 5150 |
. . . . 5
⊢ Rel
(𝑋 × 𝑋) |
47 | | relss 5129 |
. . . . 5
⊢ (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅)) |
48 | 45, 46, 47 | mpisyl 21 |
. . . 4
⊢ (𝜑 → Rel 𝑅) |
49 | | inss2 3796 |
. . . . 5
⊢ (𝑆 ∩ (𝑌 × 𝑋)) ⊆ (𝑌 × 𝑋) |
50 | | relxp 5150 |
. . . . 5
⊢ Rel
(𝑌 × 𝑋) |
51 | | relss 5129 |
. . . . 5
⊢ ((𝑆 ∩ (𝑌 × 𝑋)) ⊆ (𝑌 × 𝑋) → (Rel (𝑌 × 𝑋) → Rel (𝑆 ∩ (𝑌 × 𝑋)))) |
52 | 49, 50, 51 | mp2 9 |
. . . 4
⊢ Rel
(𝑆 ∩ (𝑌 × 𝑋)) |
53 | 48, 52 | jctir 559 |
. . 3
⊢ (𝜑 → (Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋)))) |
54 | 45 | ssbrd 4626 |
. . . . . . 7
⊢ (𝜑 → (𝑥𝑅𝑦 → 𝑥(𝑋 × 𝑋)𝑦)) |
55 | | brxp 5071 |
. . . . . . 7
⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
56 | 54, 55 | syl6ib 240 |
. . . . . 6
⊢ (𝜑 → (𝑥𝑅𝑦 → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
57 | | brinxp2 5103 |
. . . . . . . 8
⊢ (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥𝑆𝑦)) |
58 | | df-3an 1033 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥𝑆𝑦) ↔ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) |
59 | 57, 58 | bitri 263 |
. . . . . . 7
⊢ (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) |
60 | | simprll 798 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ 𝑌) |
61 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑆𝑦) |
62 | | isocnv 6480 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
63 | 36, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
65 | 43 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 ⊆ 𝑌) |
66 | | simprlr 799 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ 𝑋) |
67 | 65, 66 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ 𝑌) |
68 | | isorel 6476 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑆𝑦 ↔ (◡𝑁‘𝑥) E (◡𝑁‘𝑦))) |
69 | 64, 60, 67, 68 | syl12anc 1316 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑆𝑦 ↔ (◡𝑁‘𝑥) E (◡𝑁‘𝑦))) |
70 | 61, 69 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑥) E (◡𝑁‘𝑦)) |
71 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (◡𝑁‘𝑦) ∈ V |
72 | 71 | epelc 4951 |
. . . . . . . . . . . . 13
⊢ ((◡𝑁‘𝑥) E (◡𝑁‘𝑦) ↔ (◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦)) |
73 | 70, 72 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦)) |
74 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀)) |
75 | 74 | cnveqd 5220 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑀 = ◡(𝑁 ↾ dom 𝑀)) |
76 | | isof1o 6473 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁) → ◡𝑁:𝑌–1-1-onto→dom
𝑁) |
77 | | f1ofn 6051 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑁:𝑌–1-1-onto→dom
𝑁 → ◡𝑁 Fn 𝑌) |
78 | 64, 76, 77 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑁 Fn 𝑌) |
79 | | fnfun 5902 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑁 Fn 𝑌 → Fun ◡𝑁) |
80 | | funcnvres 5881 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡𝑁 → ◡(𝑁 ↾ dom 𝑀) = (◡𝑁 ↾ (𝑁 “ dom 𝑀))) |
81 | 78, 79, 80 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡(𝑁 ↾ dom 𝑀) = (◡𝑁 ↾ (𝑁 “ dom 𝑀))) |
82 | 75, 81 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑀 = (◡𝑁 ↾ (𝑁 “ dom 𝑀))) |
83 | 82 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑀‘𝑦) = ((◡𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦)) |
84 | 27 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀)) |
85 | 66, 84 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ (𝑁 “ dom 𝑀)) |
86 | | fvres 6117 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝑁 “ dom 𝑀) → ((◡𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (◡𝑁‘𝑦)) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ((◡𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (◡𝑁‘𝑦)) |
88 | 83, 87 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑀‘𝑦) = (◡𝑁‘𝑦)) |
89 | | isocnv 6480 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀)) |
90 | 13, 89 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀)) |
91 | | isof1o 6473 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀) → ◡𝑀:𝑋–1-1-onto→dom
𝑀) |
92 | | f1of 6050 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝑀:𝑋–1-1-onto→dom
𝑀 → ◡𝑀:𝑋⟶dom 𝑀) |
93 | 90, 91, 92 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ◡𝑀:𝑋⟶dom 𝑀) |
94 | 93 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑀:𝑋⟶dom 𝑀) |
95 | 94, 66 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑀‘𝑦) ∈ dom 𝑀) |
96 | 88, 95 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑦) ∈ dom 𝑀) |
97 | 11 | oicl 8317 |
. . . . . . . . . . . . 13
⊢ Ord dom
𝑀 |
98 | | ordtr1 5684 |
. . . . . . . . . . . . 13
⊢ (Ord dom
𝑀 → (((◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦) ∧ (◡𝑁‘𝑦) ∈ dom 𝑀) → (◡𝑁‘𝑥) ∈ dom 𝑀)) |
99 | 97, 98 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (((◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦) ∧ (◡𝑁‘𝑦) ∈ dom 𝑀) → (◡𝑁‘𝑥) ∈ dom 𝑀) |
100 | 73, 96, 99 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑥) ∈ dom 𝑀) |
101 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (◡𝑁 Fn 𝑌 → (𝑥 ∈ (◡◡𝑁 “ dom 𝑀) ↔ (𝑥 ∈ 𝑌 ∧ (◡𝑁‘𝑥) ∈ dom 𝑀))) |
102 | 78, 101 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥 ∈ (◡◡𝑁 “ dom 𝑀) ↔ (𝑥 ∈ 𝑌 ∧ (◡𝑁‘𝑥) ∈ dom 𝑀))) |
103 | 60, 100, 102 | mpbir2and 959 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ (◡◡𝑁 “ dom 𝑀)) |
104 | | imacnvcnv 5517 |
. . . . . . . . . . 11
⊢ (◡◡𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀) |
105 | 84, 104 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (◡◡𝑁 “ dom 𝑀)) |
106 | 103, 105 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ 𝑋) |
107 | 106, 66 | jca 553 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
108 | 107 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
109 | 59, 108 | syl5bi 231 |
. . . . . 6
⊢ (𝜑 → (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
110 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀)) |
111 | 110 | cnveqd 5220 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ◡𝑀 = ◡(𝑁 ↾ dom 𝑀)) |
112 | 111 | fveq1d 6105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (◡𝑀‘𝑥) = (◡(𝑁 ↾ dom 𝑀)‘𝑥)) |
113 | 111 | fveq1d 6105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (◡𝑀‘𝑦) = (◡(𝑁 ↾ dom 𝑀)‘𝑦)) |
114 | 112, 113 | breq12d 4596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((◡𝑀‘𝑥) E (◡𝑀‘𝑦) ↔ (◡(𝑁 ↾ dom 𝑀)‘𝑥) E (◡(𝑁 ↾ dom 𝑀)‘𝑦))) |
115 | | isorel 6476 |
. . . . . . . . . 10
⊢ ((◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ (◡𝑀‘𝑥) E (◡𝑀‘𝑦))) |
116 | 90, 115 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ (◡𝑀‘𝑥) E (◡𝑀‘𝑦))) |
117 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) |
118 | | isores3 6485 |
. . . . . . . . . . . . 13
⊢ ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀))) |
119 | 36, 22, 117, 118 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀))) |
120 | | isocnv 6480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)) → ◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀)) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀)) |
122 | 121 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀)) |
123 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
124 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑋 = (𝑁 “ dom 𝑀)) |
125 | 123, 124 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ (𝑁 “ dom 𝑀)) |
126 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
127 | 126, 124 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ (𝑁 “ dom 𝑀)) |
128 | | isorel 6476 |
. . . . . . . . . 10
⊢ ((◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀) ∧ (𝑥 ∈ (𝑁 “ dom 𝑀) ∧ 𝑦 ∈ (𝑁 “ dom 𝑀))) → (𝑥𝑆𝑦 ↔ (◡(𝑁 ↾ dom 𝑀)‘𝑥) E (◡(𝑁 ↾ dom 𝑀)‘𝑦))) |
129 | 122, 125,
127, 128 | syl12anc 1316 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑆𝑦 ↔ (◡(𝑁 ↾ dom 𝑀)‘𝑥) E (◡(𝑁 ↾ dom 𝑀)‘𝑦))) |
130 | 114, 116,
129 | 3bitr4d 299 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ 𝑥𝑆𝑦)) |
131 | 43 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑌) |
132 | 131 | adantrr 749 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑌) |
133 | 132, 126 | jca 553 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) |
134 | 133 | biantrurd 528 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦))) |
135 | 134, 59 | syl6bbr 277 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑆𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)) |
136 | 130, 135 | bitrd 267 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)) |
137 | 136 | ex 449 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑅𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))) |
138 | 56, 109, 137 | pm5.21ndd 368 |
. . . . 5
⊢ (𝜑 → (𝑥𝑅𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)) |
139 | | df-br 4584 |
. . . . 5
⊢ (𝑥𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
140 | | df-br 4584 |
. . . . 5
⊢ (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (𝑆 ∩ (𝑌 × 𝑋))) |
141 | 138, 139,
140 | 3bitr3g 301 |
. . . 4
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝑅 ↔ 〈𝑥, 𝑦〉 ∈ (𝑆 ∩ (𝑌 × 𝑋)))) |
142 | 141 | eqrelrdv2 5142 |
. . 3
⊢ (((Rel
𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))) ∧ 𝜑) → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) |
143 | 53, 142 | mpancom 700 |
. 2
⊢ (𝜑 → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) |
144 | 43, 143 | jca 553 |
1
⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∧ 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))) |