Proof of Theorem fpwwe2lem9
Step | Hyp | Ref
| Expression |
1 | | fpwwe2lem9.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋𝑊𝑅) |
2 | | fpwwe2.1 |
. . . . . . . . . . 11
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
3 | 2 | relopabi 5696 |
. . . . . . . . . 10
⊢ Rel 𝑊 |
4 | 3 | brrelex1i 5610 |
. . . . . . . . 9
⊢ (𝑋𝑊𝑅 → 𝑋 ∈ V) |
5 | 1, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ V) |
6 | | fpwwe2.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ V) |
7 | 2, 6 | fpwwe2lem2 10056 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
8 | 1, 7 | mpbid 234 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) |
9 | 8 | simprld 770 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 We 𝑋) |
10 | | fpwwe2lem9.m |
. . . . . . . . 9
⊢ 𝑀 = OrdIso(𝑅, 𝑋) |
11 | 10 | oiiso 9003 |
. . . . . . . 8
⊢ ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
12 | 5, 9, 11 | syl2anc 586 |
. . . . . . 7
⊢ (𝜑 → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
13 | | isof1o 7078 |
. . . . . . 7
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀–1-1-onto→𝑋) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀:dom 𝑀–1-1-onto→𝑋) |
15 | | f1ofo 6624 |
. . . . . 6
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → 𝑀:dom 𝑀–onto→𝑋) |
16 | | forn 6595 |
. . . . . 6
⊢ (𝑀:dom 𝑀–onto→𝑋 → ran 𝑀 = 𝑋) |
17 | 14, 15, 16 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝑀 = 𝑋) |
18 | | fpwwe2.3 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
19 | | fpwwe2lem9.y |
. . . . . . 7
⊢ (𝜑 → 𝑌𝑊𝑆) |
20 | | fpwwe2lem9.n |
. . . . . . 7
⊢ 𝑁 = OrdIso(𝑆, 𝑌) |
21 | | fpwwe2lem9.s |
. . . . . . 7
⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) |
22 | 2, 6, 18, 1, 19, 10, 20, 21 | fpwwe2lem8 10061 |
. . . . . 6
⊢ (𝜑 → 𝑀 = (𝑁 ↾ dom 𝑀)) |
23 | 22 | rneqd 5810 |
. . . . 5
⊢ (𝜑 → ran 𝑀 = ran (𝑁 ↾ dom 𝑀)) |
24 | 17, 23 | eqtr3d 2860 |
. . . 4
⊢ (𝜑 → 𝑋 = ran (𝑁 ↾ dom 𝑀)) |
25 | | df-ima 5570 |
. . . 4
⊢ (𝑁 “ dom 𝑀) = ran (𝑁 ↾ dom 𝑀) |
26 | 24, 25 | syl6eqr 2876 |
. . 3
⊢ (𝜑 → 𝑋 = (𝑁 “ dom 𝑀)) |
27 | | imassrn 5942 |
. . . 4
⊢ (𝑁 “ dom 𝑀) ⊆ ran 𝑁 |
28 | 3 | brrelex1i 5610 |
. . . . . . . 8
⊢ (𝑌𝑊𝑆 → 𝑌 ∈ V) |
29 | 19, 28 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ V) |
30 | 2, 6 | fpwwe2lem2 10056 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
31 | 19, 30 | mpbid 234 |
. . . . . . . 8
⊢ (𝜑 → ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))) |
32 | 31 | simprld 770 |
. . . . . . 7
⊢ (𝜑 → 𝑆 We 𝑌) |
33 | 20 | oiiso 9003 |
. . . . . . 7
⊢ ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
34 | 29, 32, 33 | syl2anc 586 |
. . . . . 6
⊢ (𝜑 → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
35 | | isof1o 7078 |
. . . . . 6
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁–1-1-onto→𝑌) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁:dom 𝑁–1-1-onto→𝑌) |
37 | | f1ofo 6624 |
. . . . 5
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → 𝑁:dom 𝑁–onto→𝑌) |
38 | | forn 6595 |
. . . . 5
⊢ (𝑁:dom 𝑁–onto→𝑌 → ran 𝑁 = 𝑌) |
39 | 36, 37, 38 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran 𝑁 = 𝑌) |
40 | 27, 39 | sseqtrid 4021 |
. . 3
⊢ (𝜑 → (𝑁 “ dom 𝑀) ⊆ 𝑌) |
41 | 26, 40 | eqsstrd 4007 |
. 2
⊢ (𝜑 → 𝑋 ⊆ 𝑌) |
42 | 8 | simplrd 768 |
. . . . 5
⊢ (𝜑 → 𝑅 ⊆ (𝑋 × 𝑋)) |
43 | | relxp 5575 |
. . . . 5
⊢ Rel
(𝑋 × 𝑋) |
44 | | relss 5658 |
. . . . 5
⊢ (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅)) |
45 | 42, 43, 44 | mpisyl 21 |
. . . 4
⊢ (𝜑 → Rel 𝑅) |
46 | | relinxp 5689 |
. . . 4
⊢ Rel
(𝑆 ∩ (𝑌 × 𝑋)) |
47 | 45, 46 | jctir 523 |
. . 3
⊢ (𝜑 → (Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋)))) |
48 | 42 | ssbrd 5111 |
. . . . . . 7
⊢ (𝜑 → (𝑥𝑅𝑦 → 𝑥(𝑋 × 𝑋)𝑦)) |
49 | | brxp 5603 |
. . . . . . 7
⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
50 | 48, 49 | syl6ib 253 |
. . . . . 6
⊢ (𝜑 → (𝑥𝑅𝑦 → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
51 | | brinxp2 5631 |
. . . . . . 7
⊢ (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) |
52 | | simprll 777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ 𝑌) |
53 | | simprr 771 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑆𝑦) |
54 | | isocnv 7085 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
55 | 34, 54 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
56 | 55 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
57 | 41 | adantr 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 ⊆ 𝑌) |
58 | | simprlr 778 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ 𝑋) |
59 | 57, 58 | sseldd 3970 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ 𝑌) |
60 | | isorel 7081 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑆𝑦 ↔ (◡𝑁‘𝑥) E (◡𝑁‘𝑦))) |
61 | 56, 52, 59, 60 | syl12anc 834 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑆𝑦 ↔ (◡𝑁‘𝑥) E (◡𝑁‘𝑦))) |
62 | 53, 61 | mpbid 234 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑥) E (◡𝑁‘𝑦)) |
63 | | fvex 6685 |
. . . . . . . . . . . . . 14
⊢ (◡𝑁‘𝑦) ∈ V |
64 | 63 | epeli 5470 |
. . . . . . . . . . . . 13
⊢ ((◡𝑁‘𝑥) E (◡𝑁‘𝑦) ↔ (◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦)) |
65 | 62, 64 | sylib 220 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦)) |
66 | 22 | adantr 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀)) |
67 | 66 | cnveqd 5748 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑀 = ◡(𝑁 ↾ dom 𝑀)) |
68 | | isof1o 7078 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁) → ◡𝑁:𝑌–1-1-onto→dom
𝑁) |
69 | | f1ofn 6618 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑁:𝑌–1-1-onto→dom
𝑁 → ◡𝑁 Fn 𝑌) |
70 | 56, 68, 69 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑁 Fn 𝑌) |
71 | | fnfun 6455 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑁 Fn 𝑌 → Fun ◡𝑁) |
72 | | funcnvres 6434 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡𝑁 → ◡(𝑁 ↾ dom 𝑀) = (◡𝑁 ↾ (𝑁 “ dom 𝑀))) |
73 | 70, 71, 72 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡(𝑁 ↾ dom 𝑀) = (◡𝑁 ↾ (𝑁 “ dom 𝑀))) |
74 | 67, 73 | eqtrd 2858 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑀 = (◡𝑁 ↾ (𝑁 “ dom 𝑀))) |
75 | 74 | fveq1d 6674 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑀‘𝑦) = ((◡𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦)) |
76 | 26 | adantr 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀)) |
77 | 58, 76 | eleqtrd 2917 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ (𝑁 “ dom 𝑀)) |
78 | 77 | fvresd 6692 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ((◡𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (◡𝑁‘𝑦)) |
79 | 75, 78 | eqtrd 2858 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑀‘𝑦) = (◡𝑁‘𝑦)) |
80 | | isocnv 7085 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀)) |
81 | 12, 80 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀)) |
82 | | isof1o 7078 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀) → ◡𝑀:𝑋–1-1-onto→dom
𝑀) |
83 | | f1of 6617 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝑀:𝑋–1-1-onto→dom
𝑀 → ◡𝑀:𝑋⟶dom 𝑀) |
84 | 81, 82, 83 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ◡𝑀:𝑋⟶dom 𝑀) |
85 | 84 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑀:𝑋⟶dom 𝑀) |
86 | 85, 58 | ffvelrnd 6854 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑀‘𝑦) ∈ dom 𝑀) |
87 | 79, 86 | eqeltrrd 2916 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑦) ∈ dom 𝑀) |
88 | 10 | oicl 8995 |
. . . . . . . . . . . . 13
⊢ Ord dom
𝑀 |
89 | | ordtr1 6236 |
. . . . . . . . . . . . 13
⊢ (Ord dom
𝑀 → (((◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦) ∧ (◡𝑁‘𝑦) ∈ dom 𝑀) → (◡𝑁‘𝑥) ∈ dom 𝑀)) |
90 | 88, 89 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (((◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦) ∧ (◡𝑁‘𝑦) ∈ dom 𝑀) → (◡𝑁‘𝑥) ∈ dom 𝑀) |
91 | 65, 87, 90 | syl2anc 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑥) ∈ dom 𝑀) |
92 | | elpreima 6830 |
. . . . . . . . . . . 12
⊢ (◡𝑁 Fn 𝑌 → (𝑥 ∈ (◡◡𝑁 “ dom 𝑀) ↔ (𝑥 ∈ 𝑌 ∧ (◡𝑁‘𝑥) ∈ dom 𝑀))) |
93 | 70, 92 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥 ∈ (◡◡𝑁 “ dom 𝑀) ↔ (𝑥 ∈ 𝑌 ∧ (◡𝑁‘𝑥) ∈ dom 𝑀))) |
94 | 52, 91, 93 | mpbir2and 711 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ (◡◡𝑁 “ dom 𝑀)) |
95 | | imacnvcnv 6065 |
. . . . . . . . . . 11
⊢ (◡◡𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀) |
96 | 76, 95 | syl6eqr 2876 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (◡◡𝑁 “ dom 𝑀)) |
97 | 94, 96 | eleqtrrd 2918 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ 𝑋) |
98 | 97, 58 | jca 514 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
99 | 98 | ex 415 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
100 | 51, 99 | syl5bi 244 |
. . . . . 6
⊢ (𝜑 → (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
101 | 22 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀)) |
102 | 101 | cnveqd 5748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ◡𝑀 = ◡(𝑁 ↾ dom 𝑀)) |
103 | 102 | fveq1d 6674 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (◡𝑀‘𝑥) = (◡(𝑁 ↾ dom 𝑀)‘𝑥)) |
104 | 102 | fveq1d 6674 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (◡𝑀‘𝑦) = (◡(𝑁 ↾ dom 𝑀)‘𝑦)) |
105 | 103, 104 | breq12d 5081 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((◡𝑀‘𝑥) E (◡𝑀‘𝑦) ↔ (◡(𝑁 ↾ dom 𝑀)‘𝑥) E (◡(𝑁 ↾ dom 𝑀)‘𝑦))) |
106 | | isorel 7081 |
. . . . . . . . . 10
⊢ ((◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ (◡𝑀‘𝑥) E (◡𝑀‘𝑦))) |
107 | 81, 106 | sylan 582 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ (◡𝑀‘𝑥) E (◡𝑀‘𝑦))) |
108 | | eqidd 2824 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) |
109 | | isores3 7090 |
. . . . . . . . . . . . 13
⊢ ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀))) |
110 | 34, 21, 108, 109 | syl3anc 1367 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀))) |
111 | | isocnv 7085 |
. . . . . . . . . . . 12
⊢ ((𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)) → ◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀)) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀)) |
113 | 112 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀)) |
114 | | simprl 769 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
115 | 26 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑋 = (𝑁 “ dom 𝑀)) |
116 | 114, 115 | eleqtrd 2917 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ (𝑁 “ dom 𝑀)) |
117 | | simprr 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
118 | 117, 115 | eleqtrd 2917 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ (𝑁 “ dom 𝑀)) |
119 | | isorel 7081 |
. . . . . . . . . 10
⊢ ((◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀) ∧ (𝑥 ∈ (𝑁 “ dom 𝑀) ∧ 𝑦 ∈ (𝑁 “ dom 𝑀))) → (𝑥𝑆𝑦 ↔ (◡(𝑁 ↾ dom 𝑀)‘𝑥) E (◡(𝑁 ↾ dom 𝑀)‘𝑦))) |
120 | 113, 116,
118, 119 | syl12anc 834 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑆𝑦 ↔ (◡(𝑁 ↾ dom 𝑀)‘𝑥) E (◡(𝑁 ↾ dom 𝑀)‘𝑦))) |
121 | 105, 107,
120 | 3bitr4d 313 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ 𝑥𝑆𝑦)) |
122 | 41 | sselda 3969 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑌) |
123 | 122 | adantrr 715 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑌) |
124 | 123, 117 | jca 514 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) |
125 | 124 | biantrurd 535 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦))) |
126 | 125, 51 | syl6bbr 291 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑆𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)) |
127 | 121, 126 | bitrd 281 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)) |
128 | 127 | ex 415 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑅𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))) |
129 | 50, 100, 128 | pm5.21ndd 383 |
. . . . 5
⊢ (𝜑 → (𝑥𝑅𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)) |
130 | | df-br 5069 |
. . . . 5
⊢ (𝑥𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
131 | | df-br 5069 |
. . . . 5
⊢ (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (𝑆 ∩ (𝑌 × 𝑋))) |
132 | 129, 130,
131 | 3bitr3g 315 |
. . . 4
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝑅 ↔ 〈𝑥, 𝑦〉 ∈ (𝑆 ∩ (𝑌 × 𝑋)))) |
133 | 132 | eqrelrdv2 5670 |
. . 3
⊢ (((Rel
𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))) ∧ 𝜑) → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) |
134 | 47, 133 | mpancom 686 |
. 2
⊢ (𝜑 → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) |
135 | 41, 134 | jca 514 |
1
⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∧ 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))) |