Proof of Theorem fpwwe2lem7
Step | Hyp | Ref
| Expression |
1 | | fpwwe2lem9.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌𝑊𝑆) |
2 | | fpwwe2.1 |
. . . . . . . . . 10
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
3 | 2 | relopabi 5167 |
. . . . . . . . 9
⊢ Rel 𝑊 |
4 | 3 | brrelexi 5082 |
. . . . . . . 8
⊢ (𝑌𝑊𝑆 → 𝑌 ∈ V) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ V) |
6 | | fpwwe2.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ V) |
7 | 2, 6 | fpwwe2lem2 9333 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
8 | 1, 7 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))) |
9 | 8 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)) |
10 | 9 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → 𝑆 We 𝑌) |
11 | | fpwwe2lem9.n |
. . . . . . . 8
⊢ 𝑁 = OrdIso(𝑆, 𝑌) |
12 | 11 | oiiso 8325 |
. . . . . . 7
⊢ ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
13 | 5, 10, 12 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
15 | | isof1o 6473 |
. . . . 5
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁–1-1-onto→𝑌) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁:dom 𝑁–1-1-onto→𝑌) |
17 | | fpwwe2.3 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
18 | | fpwwe2lem9.x |
. . . . . 6
⊢ (𝜑 → 𝑋𝑊𝑅) |
19 | | fpwwe2lem9.m |
. . . . . 6
⊢ 𝑀 = OrdIso(𝑅, 𝑋) |
20 | | fpwwe2lem7.1 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ dom 𝑀) |
21 | | fpwwe2lem7.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ dom 𝑁) |
22 | | fpwwe2lem7.3 |
. . . . . 6
⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵)) |
23 | 2, 6, 17, 18, 1, 19, 11, 20, 21, 22 | fpwwe2lem6 9336 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (◡𝑀‘𝐶) = (◡𝑁‘𝐶))) |
24 | 23 | simp2d 1067 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑌) |
25 | | f1ocnvfv2 6433 |
. . . 4
⊢ ((𝑁:dom 𝑁–1-1-onto→𝑌 ∧ 𝐶 ∈ 𝑌) → (𝑁‘(◡𝑁‘𝐶)) = 𝐶) |
26 | 16, 24, 25 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑁‘(◡𝑁‘𝐶)) = 𝐶) |
27 | 23 | simp3d 1068 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) = (◡𝑁‘𝐶)) |
28 | 3 | brrelexi 5082 |
. . . . . . . . . . . 12
⊢ (𝑋𝑊𝑅 → 𝑋 ∈ V) |
29 | 18, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ V) |
30 | 2, 6 | fpwwe2lem2 9333 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
31 | 18, 30 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) |
32 | 31 | simprd 478 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)) |
33 | 32 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 We 𝑋) |
34 | 19 | oiiso 8325 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
35 | 29, 33, 34 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
37 | | isof1o 6473 |
. . . . . . . . 9
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀–1-1-onto→𝑋) |
38 | 36, 37 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀:dom 𝑀–1-1-onto→𝑋) |
39 | 23 | simp1d 1066 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑋) |
40 | | f1ocnvfv2 6433 |
. . . . . . . 8
⊢ ((𝑀:dom 𝑀–1-1-onto→𝑋 ∧ 𝐶 ∈ 𝑋) → (𝑀‘(◡𝑀‘𝐶)) = 𝐶) |
41 | 38, 39, 40 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(◡𝑀‘𝐶)) = 𝐶) |
42 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶𝑅(𝑀‘𝐵)) |
43 | 41, 42 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵)) |
44 | | f1ocnv 6062 |
. . . . . . . . 9
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → ◡𝑀:𝑋–1-1-onto→dom
𝑀) |
45 | | f1of 6050 |
. . . . . . . . 9
⊢ (◡𝑀:𝑋–1-1-onto→dom
𝑀 → ◡𝑀:𝑋⟶dom 𝑀) |
46 | 38, 44, 45 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡𝑀:𝑋⟶dom 𝑀) |
47 | 46, 39 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) ∈ dom 𝑀) |
48 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐵 ∈ dom 𝑀) |
49 | | isorel 6476 |
. . . . . . 7
⊢ ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((◡𝑀‘𝐶) ∈ dom 𝑀 ∧ 𝐵 ∈ dom 𝑀)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵))) |
50 | 36, 47, 48, 49 | syl12anc 1316 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵))) |
51 | 43, 50 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) E 𝐵) |
52 | 27, 51 | eqbrtrrd 4607 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑁‘𝐶) E 𝐵) |
53 | | f1ocnv 6062 |
. . . . . . 7
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → ◡𝑁:𝑌–1-1-onto→dom
𝑁) |
54 | | f1of 6050 |
. . . . . . 7
⊢ (◡𝑁:𝑌–1-1-onto→dom
𝑁 → ◡𝑁:𝑌⟶dom 𝑁) |
55 | 16, 53, 54 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡𝑁:𝑌⟶dom 𝑁) |
56 | 55, 24 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑁‘𝐶) ∈ dom 𝑁) |
57 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐵 ∈ dom 𝑁) |
58 | | isorel 6476 |
. . . . 5
⊢ ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ ((◡𝑁‘𝐶) ∈ dom 𝑁 ∧ 𝐵 ∈ dom 𝑁)) → ((◡𝑁‘𝐶) E 𝐵 ↔ (𝑁‘(◡𝑁‘𝐶))𝑆(𝑁‘𝐵))) |
59 | 14, 56, 57, 58 | syl12anc 1316 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑁‘𝐶) E 𝐵 ↔ (𝑁‘(◡𝑁‘𝐶))𝑆(𝑁‘𝐵))) |
60 | 52, 59 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑁‘(◡𝑁‘𝐶))𝑆(𝑁‘𝐵)) |
61 | 26, 60 | eqbrtrrd 4607 |
. 2
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶𝑆(𝑁‘𝐵)) |
62 | 27 | adantrr 749 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (◡𝑀‘𝐶) = (◡𝑁‘𝐶)) |
63 | 2, 6, 17, 18, 1, 19, 11, 20, 21, 22 | fpwwe2lem6 9336 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → (𝐷 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ∧ (◡𝑀‘𝐷) = (◡𝑁‘𝐷))) |
64 | 63 | simp3d 1068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐷) = (◡𝑁‘𝐷)) |
65 | 64 | adantrl 748 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (◡𝑀‘𝐷) = (◡𝑁‘𝐷)) |
66 | 62, 65 | breq12d 4596 |
. . . 4
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → ((◡𝑀‘𝐶) E (◡𝑀‘𝐷) ↔ (◡𝑁‘𝐶) E (◡𝑁‘𝐷))) |
67 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
68 | | isocnv 6480 |
. . . . . 6
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀)) |
69 | 67, 68 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀)) |
70 | 39 | adantrr 749 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝐶 ∈ 𝑋) |
71 | 31 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋))) |
72 | 71 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ⊆ (𝑋 × 𝑋)) |
73 | 72 | ssbrd 4626 |
. . . . . . . 8
⊢ (𝜑 → (𝐷𝑅(𝑀‘𝐵) → 𝐷(𝑋 × 𝑋)(𝑀‘𝐵))) |
74 | 73 | imp 444 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → 𝐷(𝑋 × 𝑋)(𝑀‘𝐵)) |
75 | | brxp 5071 |
. . . . . . . 8
⊢ (𝐷(𝑋 × 𝑋)(𝑀‘𝐵) ↔ (𝐷 ∈ 𝑋 ∧ (𝑀‘𝐵) ∈ 𝑋)) |
76 | 75 | simplbi 475 |
. . . . . . 7
⊢ (𝐷(𝑋 × 𝑋)(𝑀‘𝐵) → 𝐷 ∈ 𝑋) |
77 | 74, 76 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → 𝐷 ∈ 𝑋) |
78 | 77 | adantrl 748 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝐷 ∈ 𝑋) |
79 | | isorel 6476 |
. . . . 5
⊢ ((◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (𝐶𝑅𝐷 ↔ (◡𝑀‘𝐶) E (◡𝑀‘𝐷))) |
80 | 69, 70, 78, 79 | syl12anc 1316 |
. . . 4
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (𝐶𝑅𝐷 ↔ (◡𝑀‘𝐶) E (◡𝑀‘𝐷))) |
81 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
82 | | isocnv 6480 |
. . . . . 6
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
83 | 81, 82 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁)) |
84 | 24 | adantrr 749 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝐶 ∈ 𝑌) |
85 | 63 | simp2d 1067 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → 𝐷 ∈ 𝑌) |
86 | 85 | adantrl 748 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝐷 ∈ 𝑌) |
87 | | isorel 6476 |
. . . . 5
⊢ ((◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝐶 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌)) → (𝐶𝑆𝐷 ↔ (◡𝑁‘𝐶) E (◡𝑁‘𝐷))) |
88 | 83, 84, 86, 87 | syl12anc 1316 |
. . . 4
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (𝐶𝑆𝐷 ↔ (◡𝑁‘𝐶) E (◡𝑁‘𝐷))) |
89 | 66, 80, 88 | 3bitr4d 299 |
. . 3
⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷)) |
90 | 89 | expr 641 |
. 2
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷))) |
91 | 61, 90 | jca 553 |
1
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶𝑆(𝑁‘𝐵) ∧ (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷)))) |