Proof of Theorem fpwwe2lem6
Step | Hyp | Ref
| Expression |
1 | | fpwwe2lem9.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋𝑊𝑅) |
2 | | fpwwe2.1 |
. . . . . . . . 9
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
3 | | fpwwe2.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ V) |
4 | 2, 3 | fpwwe2lem2 9333 |
. . . . . . . 8
⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
5 | 1, 4 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) |
6 | 5 | simpld 474 |
. . . . . 6
⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋))) |
7 | 6 | simprd 478 |
. . . . 5
⊢ (𝜑 → 𝑅 ⊆ (𝑋 × 𝑋)) |
8 | 7 | ssbrd 4626 |
. . . 4
⊢ (𝜑 → (𝐶𝑅(𝑀‘𝐵) → 𝐶(𝑋 × 𝑋)(𝑀‘𝐵))) |
9 | | brxp 5071 |
. . . . 5
⊢ (𝐶(𝑋 × 𝑋)(𝑀‘𝐵) ↔ (𝐶 ∈ 𝑋 ∧ (𝑀‘𝐵) ∈ 𝑋)) |
10 | 9 | simplbi 475 |
. . . 4
⊢ (𝐶(𝑋 × 𝑋)(𝑀‘𝐵) → 𝐶 ∈ 𝑋) |
11 | 8, 10 | syl6 34 |
. . 3
⊢ (𝜑 → (𝐶𝑅(𝑀‘𝐵) → 𝐶 ∈ 𝑋)) |
12 | 11 | imp 444 |
. 2
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑋) |
13 | | imassrn 5396 |
. . . 4
⊢ (𝑁 “ 𝐵) ⊆ ran 𝑁 |
14 | | fpwwe2lem9.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌𝑊𝑆) |
15 | 2 | relopabi 5167 |
. . . . . . . . . 10
⊢ Rel 𝑊 |
16 | 15 | brrelexi 5082 |
. . . . . . . . 9
⊢ (𝑌𝑊𝑆 → 𝑌 ∈ V) |
17 | 14, 16 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ V) |
18 | 2, 3 | fpwwe2lem2 9333 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
19 | 14, 18 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))) |
20 | 19 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)) |
21 | 20 | simpld 474 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 We 𝑌) |
22 | | fpwwe2lem9.n |
. . . . . . . . 9
⊢ 𝑁 = OrdIso(𝑆, 𝑌) |
23 | 22 | oiiso 8325 |
. . . . . . . 8
⊢ ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
24 | 17, 21, 23 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
26 | | isof1o 6473 |
. . . . . 6
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁–1-1-onto→𝑌) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁:dom 𝑁–1-1-onto→𝑌) |
28 | | f1ofo 6057 |
. . . . 5
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → 𝑁:dom 𝑁–onto→𝑌) |
29 | | forn 6031 |
. . . . 5
⊢ (𝑁:dom 𝑁–onto→𝑌 → ran 𝑁 = 𝑌) |
30 | 27, 28, 29 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ran 𝑁 = 𝑌) |
31 | 13, 30 | syl5sseq 3616 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑁 “ 𝐵) ⊆ 𝑌) |
32 | 15 | brrelexi 5082 |
. . . . . . . . . . . . . 14
⊢ (𝑋𝑊𝑅 → 𝑋 ∈ V) |
33 | 1, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ V) |
34 | 5 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)) |
35 | 34 | simpld 474 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 We 𝑋) |
36 | | fpwwe2lem9.m |
. . . . . . . . . . . . . 14
⊢ 𝑀 = OrdIso(𝑅, 𝑋) |
37 | 36 | oiiso 8325 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
38 | 33, 35, 37 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
39 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
40 | | isof1o 6473 |
. . . . . . . . . . 11
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀–1-1-onto→𝑋) |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀:dom 𝑀–1-1-onto→𝑋) |
42 | | f1ocnvfv2 6433 |
. . . . . . . . . 10
⊢ ((𝑀:dom 𝑀–1-1-onto→𝑋 ∧ 𝐶 ∈ 𝑋) → (𝑀‘(◡𝑀‘𝐶)) = 𝐶) |
43 | 41, 12, 42 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(◡𝑀‘𝐶)) = 𝐶) |
44 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶𝑅(𝑀‘𝐵)) |
45 | 43, 44 | eqbrtrd 4605 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵)) |
46 | | f1ocnv 6062 |
. . . . . . . . . . 11
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → ◡𝑀:𝑋–1-1-onto→dom
𝑀) |
47 | | f1of 6050 |
. . . . . . . . . . 11
⊢ (◡𝑀:𝑋–1-1-onto→dom
𝑀 → ◡𝑀:𝑋⟶dom 𝑀) |
48 | 41, 46, 47 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡𝑀:𝑋⟶dom 𝑀) |
49 | 48, 12 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) ∈ dom 𝑀) |
50 | | fpwwe2lem7.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ dom 𝑀) |
51 | 50 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐵 ∈ dom 𝑀) |
52 | | isorel 6476 |
. . . . . . . . 9
⊢ ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((◡𝑀‘𝐶) ∈ dom 𝑀 ∧ 𝐵 ∈ dom 𝑀)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵))) |
53 | 39, 49, 51, 52 | syl12anc 1316 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵))) |
54 | 45, 53 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) E 𝐵) |
55 | | epelg 4950 |
. . . . . . . 8
⊢ (𝐵 ∈ dom 𝑀 → ((◡𝑀‘𝐶) E 𝐵 ↔ (◡𝑀‘𝐶) ∈ 𝐵)) |
56 | 51, 55 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (◡𝑀‘𝐶) ∈ 𝐵)) |
57 | 54, 56 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) ∈ 𝐵) |
58 | | ffn 5958 |
. . . . . . 7
⊢ (◡𝑀:𝑋⟶dom 𝑀 → ◡𝑀 Fn 𝑋) |
59 | | elpreima 6245 |
. . . . . . 7
⊢ (◡𝑀 Fn 𝑋 → (𝐶 ∈ (◡◡𝑀 “ 𝐵) ↔ (𝐶 ∈ 𝑋 ∧ (◡𝑀‘𝐶) ∈ 𝐵))) |
60 | 48, 58, 59 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ (◡◡𝑀 “ 𝐵) ↔ (𝐶 ∈ 𝑋 ∧ (◡𝑀‘𝐶) ∈ 𝐵))) |
61 | 12, 57, 60 | mpbir2and 959 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ (◡◡𝑀 “ 𝐵)) |
62 | | imacnvcnv 5517 |
. . . . 5
⊢ (◡◡𝑀 “ 𝐵) = (𝑀 “ 𝐵) |
63 | 61, 62 | syl6eleq 2698 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ (𝑀 “ 𝐵)) |
64 | | fpwwe2lem7.3 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵)) |
65 | 64 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵)) |
66 | 65 | rneqd 5274 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ran (𝑀 ↾ 𝐵) = ran (𝑁 ↾ 𝐵)) |
67 | | df-ima 5051 |
. . . . 5
⊢ (𝑀 “ 𝐵) = ran (𝑀 ↾ 𝐵) |
68 | | df-ima 5051 |
. . . . 5
⊢ (𝑁 “ 𝐵) = ran (𝑁 ↾ 𝐵) |
69 | 66, 67, 68 | 3eqtr4g 2669 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀 “ 𝐵) = (𝑁 “ 𝐵)) |
70 | 63, 69 | eleqtrd 2690 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ (𝑁 “ 𝐵)) |
71 | 31, 70 | sseldd 3569 |
. 2
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑌) |
72 | 65 | cnveqd 5220 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡(𝑀 ↾ 𝐵) = ◡(𝑁 ↾ 𝐵)) |
73 | | dff1o3 6056 |
. . . . . . 7
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 ↔ (𝑀:dom 𝑀–onto→𝑋 ∧ Fun ◡𝑀)) |
74 | 73 | simprbi 479 |
. . . . . 6
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → Fun ◡𝑀) |
75 | | funcnvres 5881 |
. . . . . 6
⊢ (Fun
◡𝑀 → ◡(𝑀 ↾ 𝐵) = (◡𝑀 ↾ (𝑀 “ 𝐵))) |
76 | 41, 74, 75 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡(𝑀 ↾ 𝐵) = (◡𝑀 ↾ (𝑀 “ 𝐵))) |
77 | | dff1o3 6056 |
. . . . . . 7
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 ↔ (𝑁:dom 𝑁–onto→𝑌 ∧ Fun ◡𝑁)) |
78 | 77 | simprbi 479 |
. . . . . 6
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → Fun ◡𝑁) |
79 | | funcnvres 5881 |
. . . . . 6
⊢ (Fun
◡𝑁 → ◡(𝑁 ↾ 𝐵) = (◡𝑁 ↾ (𝑁 “ 𝐵))) |
80 | 27, 78, 79 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡(𝑁 ↾ 𝐵) = (◡𝑁 ↾ (𝑁 “ 𝐵))) |
81 | 72, 76, 80 | 3eqtr3d 2652 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀 ↾ (𝑀 “ 𝐵)) = (◡𝑁 ↾ (𝑁 “ 𝐵))) |
82 | 81 | fveq1d 6105 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀 ↾ (𝑀 “ 𝐵))‘𝐶) = ((◡𝑁 ↾ (𝑁 “ 𝐵))‘𝐶)) |
83 | | fvres 6117 |
. . . 4
⊢ (𝐶 ∈ (𝑀 “ 𝐵) → ((◡𝑀 ↾ (𝑀 “ 𝐵))‘𝐶) = (◡𝑀‘𝐶)) |
84 | 63, 83 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀 ↾ (𝑀 “ 𝐵))‘𝐶) = (◡𝑀‘𝐶)) |
85 | | fvres 6117 |
. . . 4
⊢ (𝐶 ∈ (𝑁 “ 𝐵) → ((◡𝑁 ↾ (𝑁 “ 𝐵))‘𝐶) = (◡𝑁‘𝐶)) |
86 | 70, 85 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑁 ↾ (𝑁 “ 𝐵))‘𝐶) = (◡𝑁‘𝐶)) |
87 | 82, 84, 86 | 3eqtr3d 2652 |
. 2
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) = (◡𝑁‘𝐶)) |
88 | 12, 71, 87 | 3jca 1235 |
1
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (◡𝑀‘𝐶) = (◡𝑁‘𝐶))) |