Proof of Theorem fpwwe2lem5
Step | Hyp | Ref
| Expression |
1 | | fpwwe2lem8.x |
. . . . . . 7
⊢ (𝜑 → 𝑋𝑊𝑅) |
2 | | fpwwe2.1 |
. . . . . . . 8
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
3 | | fpwwe2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
4 | 2, 3 | fpwwe2lem2 10132 |
. . . . . . 7
⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
5 | 1, 4 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) |
6 | 5 | simplrd 770 |
. . . . 5
⊢ (𝜑 → 𝑅 ⊆ (𝑋 × 𝑋)) |
7 | 6 | ssbrd 5073 |
. . . 4
⊢ (𝜑 → (𝐶𝑅(𝑀‘𝐵) → 𝐶(𝑋 × 𝑋)(𝑀‘𝐵))) |
8 | | brxp 5572 |
. . . . 5
⊢ (𝐶(𝑋 × 𝑋)(𝑀‘𝐵) ↔ (𝐶 ∈ 𝑋 ∧ (𝑀‘𝐵) ∈ 𝑋)) |
9 | 8 | simplbi 501 |
. . . 4
⊢ (𝐶(𝑋 × 𝑋)(𝑀‘𝐵) → 𝐶 ∈ 𝑋) |
10 | 7, 9 | syl6 35 |
. . 3
⊢ (𝜑 → (𝐶𝑅(𝑀‘𝐵) → 𝐶 ∈ 𝑋)) |
11 | 10 | imp 410 |
. 2
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑋) |
12 | | imassrn 5914 |
. . . 4
⊢ (𝑁 “ 𝐵) ⊆ ran 𝑁 |
13 | | fpwwe2lem8.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌𝑊𝑆) |
14 | 2 | relopabiv 5664 |
. . . . . . . . . 10
⊢ Rel 𝑊 |
15 | 14 | brrelex1i 5579 |
. . . . . . . . 9
⊢ (𝑌𝑊𝑆 → 𝑌 ∈ V) |
16 | 13, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ V) |
17 | 2, 3 | fpwwe2lem2 10132 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))) |
18 | 13, 17 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))) |
19 | 18 | simprld 772 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 We 𝑌) |
20 | | fpwwe2lem8.n |
. . . . . . . . 9
⊢ 𝑁 = OrdIso(𝑆, 𝑌) |
21 | 20 | oiiso 9074 |
. . . . . . . 8
⊢ ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
22 | 16, 19, 21 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
23 | 22 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌)) |
24 | | isof1o 7089 |
. . . . . 6
⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁–1-1-onto→𝑌) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁:dom 𝑁–1-1-onto→𝑌) |
26 | | f1ofo 6625 |
. . . . 5
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → 𝑁:dom 𝑁–onto→𝑌) |
27 | | forn 6595 |
. . . . 5
⊢ (𝑁:dom 𝑁–onto→𝑌 → ran 𝑁 = 𝑌) |
28 | 25, 26, 27 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ran 𝑁 = 𝑌) |
29 | 12, 28 | sseqtrid 3929 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑁 “ 𝐵) ⊆ 𝑌) |
30 | 14 | brrelex1i 5579 |
. . . . . . . . . . . . . 14
⊢ (𝑋𝑊𝑅 → 𝑋 ∈ V) |
31 | 1, 30 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ V) |
32 | 5 | simprld 772 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 We 𝑋) |
33 | | fpwwe2lem8.m |
. . . . . . . . . . . . . 14
⊢ 𝑀 = OrdIso(𝑅, 𝑋) |
34 | 33 | oiiso 9074 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
35 | 31, 32, 34 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
36 | 35 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋)) |
37 | | isof1o 7089 |
. . . . . . . . . . 11
⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀–1-1-onto→𝑋) |
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀:dom 𝑀–1-1-onto→𝑋) |
39 | | f1ocnvfv2 7045 |
. . . . . . . . . 10
⊢ ((𝑀:dom 𝑀–1-1-onto→𝑋 ∧ 𝐶 ∈ 𝑋) → (𝑀‘(◡𝑀‘𝐶)) = 𝐶) |
40 | 38, 11, 39 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(◡𝑀‘𝐶)) = 𝐶) |
41 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶𝑅(𝑀‘𝐵)) |
42 | 40, 41 | eqbrtrd 5052 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵)) |
43 | | f1ocnv 6630 |
. . . . . . . . . . 11
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → ◡𝑀:𝑋–1-1-onto→dom
𝑀) |
44 | | f1of 6618 |
. . . . . . . . . . 11
⊢ (◡𝑀:𝑋–1-1-onto→dom
𝑀 → ◡𝑀:𝑋⟶dom 𝑀) |
45 | 38, 43, 44 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡𝑀:𝑋⟶dom 𝑀) |
46 | 45, 11 | ffvelrnd 6862 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) ∈ dom 𝑀) |
47 | | fpwwe2lem5.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ dom 𝑀) |
48 | 47 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐵 ∈ dom 𝑀) |
49 | | isorel 7092 |
. . . . . . . . 9
⊢ ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((◡𝑀‘𝐶) ∈ dom 𝑀 ∧ 𝐵 ∈ dom 𝑀)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵))) |
50 | 36, 46, 48, 49 | syl12anc 836 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵))) |
51 | 42, 50 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) E 𝐵) |
52 | | epelg 5435 |
. . . . . . . 8
⊢ (𝐵 ∈ dom 𝑀 → ((◡𝑀‘𝐶) E 𝐵 ↔ (◡𝑀‘𝐶) ∈ 𝐵)) |
53 | 48, 52 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (◡𝑀‘𝐶) ∈ 𝐵)) |
54 | 51, 53 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) ∈ 𝐵) |
55 | | ffn 6504 |
. . . . . . 7
⊢ (◡𝑀:𝑋⟶dom 𝑀 → ◡𝑀 Fn 𝑋) |
56 | | elpreima 6835 |
. . . . . . 7
⊢ (◡𝑀 Fn 𝑋 → (𝐶 ∈ (◡◡𝑀 “ 𝐵) ↔ (𝐶 ∈ 𝑋 ∧ (◡𝑀‘𝐶) ∈ 𝐵))) |
57 | 45, 55, 56 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ (◡◡𝑀 “ 𝐵) ↔ (𝐶 ∈ 𝑋 ∧ (◡𝑀‘𝐶) ∈ 𝐵))) |
58 | 11, 54, 57 | mpbir2and 713 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ (◡◡𝑀 “ 𝐵)) |
59 | | imacnvcnv 6038 |
. . . . 5
⊢ (◡◡𝑀 “ 𝐵) = (𝑀 “ 𝐵) |
60 | 58, 59 | eleqtrdi 2843 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ (𝑀 “ 𝐵)) |
61 | | fpwwe2lem5.3 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵)) |
62 | 61 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵)) |
63 | 62 | rneqd 5781 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ran (𝑀 ↾ 𝐵) = ran (𝑁 ↾ 𝐵)) |
64 | | df-ima 5538 |
. . . . 5
⊢ (𝑀 “ 𝐵) = ran (𝑀 ↾ 𝐵) |
65 | | df-ima 5538 |
. . . . 5
⊢ (𝑁 “ 𝐵) = ran (𝑁 ↾ 𝐵) |
66 | 63, 64, 65 | 3eqtr4g 2798 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀 “ 𝐵) = (𝑁 “ 𝐵)) |
67 | 60, 66 | eleqtrd 2835 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ (𝑁 “ 𝐵)) |
68 | 29, 67 | sseldd 3878 |
. 2
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑌) |
69 | 62 | cnveqd 5718 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡(𝑀 ↾ 𝐵) = ◡(𝑁 ↾ 𝐵)) |
70 | | dff1o3 6624 |
. . . . . . 7
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 ↔ (𝑀:dom 𝑀–onto→𝑋 ∧ Fun ◡𝑀)) |
71 | 70 | simprbi 500 |
. . . . . 6
⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → Fun ◡𝑀) |
72 | | funcnvres 6417 |
. . . . . 6
⊢ (Fun
◡𝑀 → ◡(𝑀 ↾ 𝐵) = (◡𝑀 ↾ (𝑀 “ 𝐵))) |
73 | 38, 71, 72 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡(𝑀 ↾ 𝐵) = (◡𝑀 ↾ (𝑀 “ 𝐵))) |
74 | | dff1o3 6624 |
. . . . . . 7
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 ↔ (𝑁:dom 𝑁–onto→𝑌 ∧ Fun ◡𝑁)) |
75 | 74 | simprbi 500 |
. . . . . 6
⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → Fun ◡𝑁) |
76 | | funcnvres 6417 |
. . . . . 6
⊢ (Fun
◡𝑁 → ◡(𝑁 ↾ 𝐵) = (◡𝑁 ↾ (𝑁 “ 𝐵))) |
77 | 25, 75, 76 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡(𝑁 ↾ 𝐵) = (◡𝑁 ↾ (𝑁 “ 𝐵))) |
78 | 69, 73, 77 | 3eqtr3d 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀 ↾ (𝑀 “ 𝐵)) = (◡𝑁 ↾ (𝑁 “ 𝐵))) |
79 | 78 | fveq1d 6676 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀 ↾ (𝑀 “ 𝐵))‘𝐶) = ((◡𝑁 ↾ (𝑁 “ 𝐵))‘𝐶)) |
80 | 60 | fvresd 6694 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀 ↾ (𝑀 “ 𝐵))‘𝐶) = (◡𝑀‘𝐶)) |
81 | 67 | fvresd 6694 |
. . 3
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑁 ↾ (𝑁 “ 𝐵))‘𝐶) = (◡𝑁‘𝐶)) |
82 | 79, 80, 81 | 3eqtr3d 2781 |
. 2
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) = (◡𝑁‘𝐶)) |
83 | 11, 68, 82 | 3jca 1129 |
1
⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (◡𝑀‘𝐶) = (◡𝑁‘𝐶))) |