Proof of Theorem fpwwe2lem8
| Step | Hyp | Ref
| Expression |
| 1 | | fpwwe2lem8.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋𝑊𝑅) |
| 2 | | fpwwe2.1 |
. . . . . . . . . 10
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
| 3 | 2 | relopabiv 5830 |
. . . . . . . . 9
⊢ Rel 𝑊 |
| 4 | 3 | brrelex1i 5741 |
. . . . . . . 8
⊢ (𝑋𝑊𝑅 → 𝑋 ∈ V) |
| 5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ V) |
| 6 | | fpwwe2.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 7 | 2, 6 | fpwwe2lem2 10672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
| 8 | 1, 7 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) |
| 9 | 8 | simprld 772 |
. . . . . . 7
⊢ (𝜑 → 𝑅 We 𝑋) |
| 10 | | fpwwe2lem8.m |
. . . . . . . 8
⊢ 𝑀 = OrdIso(𝑅, 𝑋) |
| 11 | 10 | oiiso 9577 |
. . . . . . 7
⊢ ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
| 12 | 5, 9, 11 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
| 13 | | isof1o 7343 |
. . . . . 6
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀–1-1-onto→𝑋) |
| 14 | | f1ofo 6855 |
. . . . . 6
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → 𝑀:dom 𝑀–onto→𝑋) |
| 15 | | forn 6823 |
. . . . . 6
⊢ (𝑀:dom 𝑀–onto→𝑋 → ran 𝑀 = 𝑋) |
| 16 | 12, 13, 14, 15 | 4syl 19 |
. . . . 5
⊢ (𝜑 → ran 𝑀 = 𝑋) |
| 17 | | fpwwe2.3 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
| 18 | | fpwwe2lem8.y |
. . . . . . 7
⊢ (𝜑 → 𝑌𝑊𝑆) |
| 19 | | fpwwe2lem8.n |
. . . . . . 7
⊢ 𝑁 = OrdIso(𝑆, 𝑌) |
| 20 | | fpwwe2lem8.s |
. . . . . . 7
⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) |
| 21 | 2, 6, 17, 1, 18, 10, 19, 20 | fpwwe2lem7 10677 |
. . . . . 6
⊢ (𝜑 → 𝑀 = (𝑁 ↾ dom 𝑀)) |
| 22 | 21 | rneqd 5949 |
. . . . 5
⊢ (𝜑 → ran 𝑀 = ran (𝑁 ↾ dom 𝑀)) |
| 23 | 16, 22 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → 𝑋 = ran (𝑁 ↾ dom 𝑀)) |
| 24 | | df-ima 5698 |
. . . 4
⊢ (𝑁 “ dom 𝑀) = ran (𝑁 ↾ dom 𝑀) |
| 25 | 23, 24 | eqtr4di 2795 |
. . 3
⊢ (𝜑 → 𝑋 = (𝑁 “ dom 𝑀)) |
| 26 | | imassrn 6089 |
. . . 4
⊢ (𝑁 “ dom 𝑀) ⊆ ran 𝑁 |
| 27 | 3 | brrelex1i 5741 |
. . . . . . 7
⊢ (𝑌𝑊𝑆 → 𝑌 ∈ V) |
| 28 | 18, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ V) |
| 29 | 2, 6 | fpwwe2lem2 10672 |
. . . . . . . 8
⊢ (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
| 30 | 18, 29 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))) |
| 31 | 30 | simprld 772 |
. . . . . 6
⊢ (𝜑 → 𝑆 We 𝑌) |
| 32 | 19 | oiiso 9577 |
. . . . . 6
⊢ ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
| 33 | 28, 31, 32 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
| 34 | | isof1o 7343 |
. . . . 5
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁–1-1-onto→𝑌) |
| 35 | | f1ofo 6855 |
. . . . 5
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → 𝑁:dom 𝑁–onto→𝑌) |
| 36 | | forn 6823 |
. . . . 5
⊢ (𝑁:dom 𝑁–onto→𝑌 → ran 𝑁 = 𝑌) |
| 37 | 33, 34, 35, 36 | 4syl 19 |
. . . 4
⊢ (𝜑 → ran 𝑁 = 𝑌) |
| 38 | 26, 37 | sseqtrid 4026 |
. . 3
⊢ (𝜑 → (𝑁 “ dom 𝑀) ⊆ 𝑌) |
| 39 | 25, 38 | eqsstrd 4018 |
. 2
⊢ (𝜑 → 𝑋 ⊆ 𝑌) |
| 40 | 8 | simplrd 770 |
. . . . 5
⊢ (𝜑 → 𝑅 ⊆ (𝑋 × 𝑋)) |
| 41 | | relxp 5703 |
. . . . 5
⊢ Rel
(𝑋 × 𝑋) |
| 42 | | relss 5791 |
. . . . 5
⊢ (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅)) |
| 43 | 40, 41, 42 | mpisyl 21 |
. . . 4
⊢ (𝜑 → Rel 𝑅) |
| 44 | | relinxp 5824 |
. . . 4
⊢ Rel
(𝑆 ∩ (𝑌 × 𝑋)) |
| 45 | 43, 44 | jctir 520 |
. . 3
⊢ (𝜑 → (Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋)))) |
| 46 | 40 | ssbrd 5186 |
. . . . . . 7
⊢ (𝜑 → (𝑥𝑅𝑦 → 𝑥(𝑋 × 𝑋)𝑦)) |
| 47 | | brxp 5734 |
. . . . . . 7
⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
| 48 | 46, 47 | imbitrdi 251 |
. . . . . 6
⊢ (𝜑 → (𝑥𝑅𝑦 → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
| 49 | | brinxp2 5763 |
. . . . . . 7
⊢ (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) |
| 50 | | isocnv 7350 |
. . . . . . . . . . . . . 14
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
| 51 | 33, 50 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
| 52 | 51 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
| 53 | | isof1o 7343 |
. . . . . . . . . . . 12
⊢ (◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁) → ◡𝑁:𝑌–1-1-onto→dom
𝑁) |
| 54 | | f1ofn 6849 |
. . . . . . . . . . . 12
⊢ (◡𝑁:𝑌–1-1-onto→dom
𝑁 → ◡𝑁 Fn 𝑌) |
| 55 | 52, 53, 54 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑁 Fn 𝑌) |
| 56 | | simprll 779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ 𝑌) |
| 57 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑆𝑦) |
| 58 | 39 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 ⊆ 𝑌) |
| 59 | | simprlr 780 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ 𝑋) |
| 60 | 58, 59 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ 𝑌) |
| 61 | | isorel 7346 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑆𝑦 ↔ (◡𝑁‘𝑥) E (◡𝑁‘𝑦))) |
| 62 | 52, 56, 60, 61 | syl12anc 837 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑆𝑦 ↔ (◡𝑁‘𝑥) E (◡𝑁‘𝑦))) |
| 63 | 57, 62 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑥) E (◡𝑁‘𝑦)) |
| 64 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢ (◡𝑁‘𝑦) ∈ V |
| 65 | 64 | epeli 5586 |
. . . . . . . . . . . . 13
⊢ ((◡𝑁‘𝑥) E (◡𝑁‘𝑦) ↔ (◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦)) |
| 66 | 63, 65 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦)) |
| 67 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀)) |
| 68 | 67 | cnveqd 5886 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑀 = ◡(𝑁 ↾ dom 𝑀)) |
| 69 | | fnfun 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑁 Fn 𝑌 → Fun ◡𝑁) |
| 70 | | funcnvres 6644 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡𝑁 → ◡(𝑁 ↾ dom 𝑀) = (◡𝑁 ↾ (𝑁 “ dom 𝑀))) |
| 71 | 55, 69, 70 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡(𝑁 ↾ dom 𝑀) = (◡𝑁 ↾ (𝑁 “ dom 𝑀))) |
| 72 | 68, 71 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑀 = (◡𝑁 ↾ (𝑁 “ dom 𝑀))) |
| 73 | 72 | fveq1d 6908 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑀‘𝑦) = ((◡𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦)) |
| 74 | 25 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀)) |
| 75 | 59, 74 | eleqtrd 2843 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ (𝑁 “ dom 𝑀)) |
| 76 | 75 | fvresd 6926 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ((◡𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (◡𝑁‘𝑦)) |
| 77 | 73, 76 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑀‘𝑦) = (◡𝑁‘𝑦)) |
| 78 | | isocnv 7350 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀)) |
| 79 | | isof1o 7343 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀) → ◡𝑀:𝑋–1-1-onto→dom
𝑀) |
| 80 | | f1of 6848 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝑀:𝑋–1-1-onto→dom
𝑀 → ◡𝑀:𝑋⟶dom 𝑀) |
| 81 | 12, 78, 79, 80 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ◡𝑀:𝑋⟶dom 𝑀) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → ◡𝑀:𝑋⟶dom 𝑀) |
| 83 | 82, 59 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑀‘𝑦) ∈ dom 𝑀) |
| 84 | 77, 83 | eqeltrrd 2842 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑦) ∈ dom 𝑀) |
| 85 | 10 | oicl 9569 |
. . . . . . . . . . . . 13
⊢ Ord dom
𝑀 |
| 86 | | ordtr1 6427 |
. . . . . . . . . . . . 13
⊢ (Ord dom
𝑀 → (((◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦) ∧ (◡𝑁‘𝑦) ∈ dom 𝑀) → (◡𝑁‘𝑥) ∈ dom 𝑀)) |
| 87 | 85, 86 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (((◡𝑁‘𝑥) ∈ (◡𝑁‘𝑦) ∧ (◡𝑁‘𝑦) ∈ dom 𝑀) → (◡𝑁‘𝑥) ∈ dom 𝑀) |
| 88 | 66, 84, 87 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (◡𝑁‘𝑥) ∈ dom 𝑀) |
| 89 | 55, 56, 88 | elpreimad 7079 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ (◡◡𝑁 “ dom 𝑀)) |
| 90 | | imacnvcnv 6226 |
. . . . . . . . . . 11
⊢ (◡◡𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀) |
| 91 | 74, 90 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (◡◡𝑁 “ dom 𝑀)) |
| 92 | 89, 91 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ 𝑋) |
| 93 | 92, 59 | jca 511 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
| 94 | 93 | ex 412 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
| 95 | 49, 94 | biimtrid 242 |
. . . . . 6
⊢ (𝜑 → (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
| 96 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀)) |
| 97 | 96 | cnveqd 5886 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ◡𝑀 = ◡(𝑁 ↾ dom 𝑀)) |
| 98 | 97 | fveq1d 6908 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (◡𝑀‘𝑥) = (◡(𝑁 ↾ dom 𝑀)‘𝑥)) |
| 99 | 97 | fveq1d 6908 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (◡𝑀‘𝑦) = (◡(𝑁 ↾ dom 𝑀)‘𝑦)) |
| 100 | 98, 99 | breq12d 5156 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((◡𝑀‘𝑥) E (◡𝑀‘𝑦) ↔ (◡(𝑁 ↾ dom 𝑀)‘𝑥) E (◡(𝑁 ↾ dom 𝑀)‘𝑦))) |
| 101 | 12, 78 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀)) |
| 102 | | isorel 7346 |
. . . . . . . . . 10
⊢ ((◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ (◡𝑀‘𝑥) E (◡𝑀‘𝑦))) |
| 103 | 101, 102 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ (◡𝑀‘𝑥) E (◡𝑀‘𝑦))) |
| 104 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) |
| 105 | | isores3 7355 |
. . . . . . . . . . . . 13
⊢ ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀))) |
| 106 | 33, 20, 104, 105 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀))) |
| 107 | | isocnv 7350 |
. . . . . . . . . . . 12
⊢ ((𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)) → ◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀)) |
| 108 | 106, 107 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀)) |
| 109 | 108 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀)) |
| 110 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
| 111 | 25 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑋 = (𝑁 “ dom 𝑀)) |
| 112 | 110, 111 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ (𝑁 “ dom 𝑀)) |
| 113 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
| 114 | 113, 111 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ (𝑁 “ dom 𝑀)) |
| 115 | | isorel 7346 |
. . . . . . . . . 10
⊢ ((◡(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀) ∧ (𝑥 ∈ (𝑁 “ dom 𝑀) ∧ 𝑦 ∈ (𝑁 “ dom 𝑀))) → (𝑥𝑆𝑦 ↔ (◡(𝑁 ↾ dom 𝑀)‘𝑥) E (◡(𝑁 ↾ dom 𝑀)‘𝑦))) |
| 116 | 109, 112,
114, 115 | syl12anc 837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑆𝑦 ↔ (◡(𝑁 ↾ dom 𝑀)‘𝑥) E (◡(𝑁 ↾ dom 𝑀)‘𝑦))) |
| 117 | 100, 103,
116 | 3bitr4d 311 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ 𝑥𝑆𝑦)) |
| 118 | 39 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑌) |
| 119 | 118 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑌) |
| 120 | 119, 113 | jca 511 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) |
| 121 | 120 | biantrurd 532 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) ∧ 𝑥𝑆𝑦))) |
| 122 | 121, 49 | bitr4di 289 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑆𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)) |
| 123 | 117, 122 | bitrd 279 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑅𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)) |
| 124 | 123 | ex 412 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑅𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))) |
| 125 | 48, 95, 124 | pm5.21ndd 379 |
. . . . 5
⊢ (𝜑 → (𝑥𝑅𝑦 ↔ 𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)) |
| 126 | | df-br 5144 |
. . . . 5
⊢ (𝑥𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
| 127 | | df-br 5144 |
. . . . 5
⊢ (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (𝑆 ∩ (𝑌 × 𝑋))) |
| 128 | 125, 126,
127 | 3bitr3g 313 |
. . . 4
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝑅 ↔ 〈𝑥, 𝑦〉 ∈ (𝑆 ∩ (𝑌 × 𝑋)))) |
| 129 | 128 | eqrelrdv2 5805 |
. . 3
⊢ (((Rel
𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))) ∧ 𝜑) → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) |
| 130 | 45, 129 | mpancom 688 |
. 2
⊢ (𝜑 → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) |
| 131 | 39, 130 | jca 511 |
1
⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∧ 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))) |