Proof of Theorem sbthlem1
Step | Hyp | Ref
| Expression |
1 | | df-f1 4792 |
. . . . . . . . 9
⊢ (R:dom R–1-1→ran R
↔ (R:dom R–→ran R ∧ Fun ◡R)) |
2 | | ssid 3290 |
. . . . . . . . . . . 12
⊢ ran R ⊆ ran R |
3 | | df-f 4791 |
. . . . . . . . . . . 12
⊢ (R:dom R–→ran R ↔ (R Fn
dom R ∧
ran R ⊆
ran R)) |
4 | 2, 3 | mpbiran2 885 |
. . . . . . . . . . 11
⊢ (R:dom R–→ran R ↔ R Fn
dom R) |
5 | | funfn 5136 |
. . . . . . . . . . 11
⊢ (Fun R ↔ R Fn
dom R) |
6 | 4, 5 | bitr4i 243 |
. . . . . . . . . 10
⊢ (R:dom R–→ran R ↔ Fun R) |
7 | 6 | anbi1i 676 |
. . . . . . . . 9
⊢ ((R:dom R–→ran R ∧ Fun ◡R)
↔ (Fun R ∧ Fun ◡R)) |
8 | 1, 7 | bitri 240 |
. . . . . . . 8
⊢ (R:dom R–1-1→ran R
↔ (Fun R ∧ Fun ◡R)) |
9 | 8 | biimpri 197 |
. . . . . . 7
⊢ ((Fun R ∧ Fun ◡R)
→ R:dom R–1-1→ran R) |
10 | | sbthlem1.4 |
. . . . . . . . 9
⊢ A = (X ∩
G) |
11 | | inss1 3475 |
. . . . . . . . . 10
⊢ (X ∩ G) ⊆ X |
12 | | sstr 3280 |
. . . . . . . . . 10
⊢ (((X ∩ G) ⊆ X ∧ X ⊆ dom R)
→ (X ∩ G) ⊆ dom R) |
13 | 11, 12 | mpan 651 |
. . . . . . . . 9
⊢ (X ⊆ dom R → (X
∩ G) ⊆ dom R) |
14 | 10, 13 | syl5eqss 3315 |
. . . . . . . 8
⊢ (X ⊆ dom R → A ⊆ dom R) |
15 | 14 | adantr 451 |
. . . . . . 7
⊢ ((X ⊆ dom R ∧ ran R ⊆ X) → A
⊆ dom R) |
16 | | f1ores 5300 |
. . . . . . 7
⊢ ((R:dom R–1-1→ran R ∧ A ⊆ dom R)
→ (R ↾ A):A–1-1-onto→(R “
A)) |
17 | 9, 15, 16 | syl2an 463 |
. . . . . 6
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(R ↾
A):A–1-1-onto→(R “
A)) |
18 | | sbthlem1.1 |
. . . . . . . 8
⊢ R ∈
V |
19 | | sbthlem1.2 |
. . . . . . . . . 10
⊢ X ∈
V |
20 | | sbthlem1.3 |
. . . . . . . . . . 11
⊢ G = Clos1 ((X ∖ ran R), R) |
21 | 18 | rnex 5107 |
. . . . . . . . . . . . 13
⊢ ran R ∈
V |
22 | 19, 21 | difex 4107 |
. . . . . . . . . . . 12
⊢ (X ∖ ran R) ∈
V |
23 | 22, 18 | clos1ex 5876 |
. . . . . . . . . . 11
⊢ Clos1 ((X ∖ ran R),
R) ∈
V |
24 | 20, 23 | eqeltri 2423 |
. . . . . . . . . 10
⊢ G ∈
V |
25 | 19, 24 | inex 4105 |
. . . . . . . . 9
⊢ (X ∩ G) ∈ V |
26 | 10, 25 | eqeltri 2423 |
. . . . . . . 8
⊢ A ∈
V |
27 | 18, 26 | resex 5117 |
. . . . . . 7
⊢ (R ↾ A) ∈
V |
28 | 27 | f1oen 6033 |
. . . . . 6
⊢ ((R ↾ A):A–1-1-onto→(R “
A) → A ≈ (R
“ A)) |
29 | 17, 28 | syl 15 |
. . . . 5
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
A ≈ (R “ A)) |
30 | | sbthlem1.6 |
. . . . . . . . 9
⊢ C = (ran R ∩
G) |
31 | 22, 18, 20 | clos1baseima 5883 |
. . . . . . . . . 10
⊢ G = ((X ∖ ran R) ∪
(R “ G)) |
32 | 31 | ineq2i 3454 |
. . . . . . . . 9
⊢ (ran R ∩ G) =
(ran R ∩ ((X ∖ ran R) ∪ (R
“ G))) |
33 | | indi 3501 |
. . . . . . . . . 10
⊢ (ran R ∩ ((X
∖ ran R)
∪ (R “ G))) = ((ran R
∩ (X ∖ ran R))
∪ (ran R ∩ (R “ G))) |
34 | | disjdif 3622 |
. . . . . . . . . . 11
⊢ (ran R ∩ (X ∖ ran R)) =
∅ |
35 | 34 | uneq1i 3414 |
. . . . . . . . . 10
⊢ ((ran R ∩ (X ∖ ran R))
∪ (ran R ∩ (R “ G))) =
(∅ ∪ (ran R ∩ (R
“ G))) |
36 | | uncom 3408 |
. . . . . . . . . . 11
⊢ (∅ ∪ (ran R
∩ (R “ G))) = ((ran R
∩ (R “ G)) ∪ ∅) |
37 | | un0 3575 |
. . . . . . . . . . 11
⊢ ((ran R ∩ (R
“ G)) ∪ ∅) = (ran R
∩ (R “ G)) |
38 | 36, 37 | eqtri 2373 |
. . . . . . . . . 10
⊢ (∅ ∪ (ran R
∩ (R “ G))) = (ran R
∩ (R “ G)) |
39 | 33, 35, 38 | 3eqtri 2377 |
. . . . . . . . 9
⊢ (ran R ∩ ((X
∖ ran R)
∪ (R “ G))) = (ran R
∩ (R “ G)) |
40 | 30, 32, 39 | 3eqtri 2377 |
. . . . . . . 8
⊢ C = (ran R ∩
(R “ G)) |
41 | | inss2 3476 |
. . . . . . . . 9
⊢ (ran R ∩ (R
“ G)) ⊆ (R “
G) |
42 | 41 | a1i 10 |
. . . . . . . 8
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(ran R ∩ (R “ G))
⊆ (R
“ G)) |
43 | 40, 42 | syl5eqss 3315 |
. . . . . . 7
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
C ⊆
(R “ G)) |
44 | | imassrn 5009 |
. . . . . . . . . . . . . 14
⊢ (R “ G)
⊆ ran R |
45 | | simprr 733 |
. . . . . . . . . . . . . 14
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
ran R ⊆
X) |
46 | 44, 45 | syl5ss 3283 |
. . . . . . . . . . . . 13
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(R “ G) ⊆ X) |
47 | | difss 3393 |
. . . . . . . . . . . . 13
⊢ (X ∖ ran R) ⊆ X |
48 | 46, 47 | jctil 523 |
. . . . . . . . . . . 12
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
((X ∖
ran R) ⊆
X ∧
(R “ G) ⊆ X)) |
49 | | unss 3437 |
. . . . . . . . . . . 12
⊢ (((X ∖ ran R) ⊆ X ∧ (R “ G)
⊆ X)
↔ ((X ∖ ran R) ∪
(R “ G)) ⊆ X) |
50 | 48, 49 | sylib 188 |
. . . . . . . . . . 11
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
((X ∖
ran R) ∪ (R “ G))
⊆ X) |
51 | 31, 50 | syl5eqss 3315 |
. . . . . . . . . 10
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
G ⊆
X) |
52 | | sseqin2 3474 |
. . . . . . . . . 10
⊢ (G ⊆ X ↔ (X
∩ G) = G) |
53 | 51, 52 | sylib 188 |
. . . . . . . . 9
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(X ∩ G) = G) |
54 | 10, 53 | syl5eq 2397 |
. . . . . . . 8
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
A = G) |
55 | 54 | imaeq2d 4942 |
. . . . . . 7
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(R “ A) = (R “
G)) |
56 | 43, 55 | sseqtr4d 3308 |
. . . . . 6
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
C ⊆
(R “ A)) |
57 | | ssun2 3427 |
. . . . . . . . . . 11
⊢ (R “ G)
⊆ ((X
∖ ran R)
∪ (R “ G)) |
58 | 57, 31 | sseqtr4i 3304 |
. . . . . . . . . 10
⊢ (R “ G)
⊆ G |
59 | 55 | sseq1d 3298 |
. . . . . . . . . 10
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
((R “ A) ⊆ G ↔ (R
“ G) ⊆ G)) |
60 | 58, 59 | mpbiri 224 |
. . . . . . . . 9
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(R “ A) ⊆ G) |
61 | | imassrn 5009 |
. . . . . . . . 9
⊢ (R “ A)
⊆ ran R |
62 | 60, 61 | jctil 523 |
. . . . . . . 8
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
((R “ A) ⊆ ran R ∧ (R “ A)
⊆ G)) |
63 | | ssin 3477 |
. . . . . . . 8
⊢ (((R “ A)
⊆ ran R
∧ (R
“ A) ⊆ G) ↔
(R “ A) ⊆ (ran
R ∩ G)) |
64 | 62, 63 | sylib 188 |
. . . . . . 7
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(R “ A) ⊆ (ran
R ∩ G)) |
65 | 64, 30 | syl6sseqr 3318 |
. . . . . 6
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(R “ A) ⊆ C) |
66 | 56, 65 | eqssd 3289 |
. . . . 5
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
C = (R
“ A)) |
67 | 29, 66 | breqtrrd 4665 |
. . . 4
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
A ≈ C) |
68 | | sbthlem1.5 |
. . . . . . 7
⊢ B = (X ∖ G) |
69 | 19, 24 | difex 4107 |
. . . . . . 7
⊢ (X ∖ G) ∈
V |
70 | 68, 69 | eqeltri 2423 |
. . . . . 6
⊢ B ∈
V |
71 | 70 | enrflx 6035 |
. . . . 5
⊢ B ≈ B |
72 | | difsscompl 3549 |
. . . . . . . . . 10
⊢ (X ∖ G) ⊆ ∼
G |
73 | 72 | a1i 10 |
. . . . . . . . 9
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(X ∖
G) ⊆
∼ G) |
74 | | df-dif 3215 |
. . . . . . . . . . 11
⊢ (X ∖ G) = (X ∩
∼ G) |
75 | 20 | clos1base 5878 |
. . . . . . . . . . . . . 14
⊢ (X ∖ ran R) ⊆ G |
76 | | sscon34 3661 |
. . . . . . . . . . . . . 14
⊢ ((X ∖ ran R) ⊆ G ↔ ∼ G
⊆ ∼ (X ∖ ran R)) |
77 | 75, 76 | mpbi 199 |
. . . . . . . . . . . . 13
⊢ ∼ G ⊆ ∼
(X ∖ ran
R) |
78 | | df-dif 3215 |
. . . . . . . . . . . . . . 15
⊢ (X ∖ ran R) = (X ∩
∼ ran R) |
79 | 78 | compleqi 3244 |
. . . . . . . . . . . . . 14
⊢ ∼ (X ∖ ran R) = ∼ (X
∩ ∼ ran R) |
80 | | iinun 3548 |
. . . . . . . . . . . . . 14
⊢ ∼ (X ∩ ∼ ran R) = ( ∼ X
∪ ∼ ∼ ran R) |
81 | | dblcompl 3227 |
. . . . . . . . . . . . . . 15
⊢ ∼ ∼ ran
R = ran R |
82 | 81 | uneq2i 3415 |
. . . . . . . . . . . . . 14
⊢ ( ∼ X ∪ ∼ ∼ ran R) = ( ∼ X
∪ ran R) |
83 | 79, 80, 82 | 3eqtri 2377 |
. . . . . . . . . . . . 13
⊢ ∼ (X ∖ ran R) = ( ∼ X
∪ ran R) |
84 | 77, 83 | sseqtri 3303 |
. . . . . . . . . . . 12
⊢ ∼ G ⊆ ( ∼
X ∪ ran R) |
85 | | sslin 3481 |
. . . . . . . . . . . 12
⊢ ( ∼ G ⊆ ( ∼
X ∪ ran R) → (X
∩ ∼ G) ⊆ (X ∩ (
∼ X ∪ ran R))) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (X ∩ ∼ G)
⊆ (X
∩ ( ∼ X ∪ ran R)) |
87 | 74, 86 | eqsstri 3301 |
. . . . . . . . . 10
⊢ (X ∖ G) ⊆ (X ∩ ( ∼ X ∪ ran R)) |
88 | | indi 3501 |
. . . . . . . . . . . 12
⊢ (X ∩ ( ∼ X ∪ ran R))
= ((X ∩ ∼ X) ∪ (X
∩ ran R)) |
89 | | incompl 4073 |
. . . . . . . . . . . . 13
⊢ (X ∩ ∼ X)
= ∅ |
90 | 89 | uneq1i 3414 |
. . . . . . . . . . . 12
⊢ ((X ∩ ∼ X)
∪ (X ∩ ran R)) = (∅ ∪
(X ∩ ran R)) |
91 | | uncom 3408 |
. . . . . . . . . . . . 13
⊢ (∅ ∪ (X
∩ ran R)) = ((X ∩ ran R)
∪ ∅) |
92 | | un0 3575 |
. . . . . . . . . . . . 13
⊢ ((X ∩ ran R)
∪ ∅) = (X ∩ ran R) |
93 | 91, 92 | eqtri 2373 |
. . . . . . . . . . . 12
⊢ (∅ ∪ (X
∩ ran R)) = (X ∩ ran R) |
94 | 88, 90, 93 | 3eqtri 2377 |
. . . . . . . . . . 11
⊢ (X ∩ ( ∼ X ∪ ran R))
= (X ∩ ran R) |
95 | | inss2 3476 |
. . . . . . . . . . 11
⊢ (X ∩ ran R)
⊆ ran R |
96 | 94, 95 | eqsstri 3301 |
. . . . . . . . . 10
⊢ (X ∩ ( ∼ X ∪ ran R))
⊆ ran R |
97 | 87, 96 | sstri 3281 |
. . . . . . . . 9
⊢ (X ∖ G) ⊆ ran R |
98 | 73, 97 | jctil 523 |
. . . . . . . 8
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
((X ∖
G) ⊆ ran
R ∧
(X ∖
G) ⊆
∼ G)) |
99 | | ssin 3477 |
. . . . . . . 8
⊢ (((X ∖ G) ⊆ ran R ∧ (X ∖ G) ⊆ ∼
G) ↔ (X ∖ G) ⊆ (ran
R ∩ ∼ G)) |
100 | 98, 99 | sylib 188 |
. . . . . . 7
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(X ∖
G) ⊆
(ran R ∩ ∼ G)) |
101 | | sbthlem1.7 |
. . . . . . . 8
⊢ D = (ran R ∖ G) |
102 | | df-dif 3215 |
. . . . . . . 8
⊢ (ran R ∖ G) = (ran R
∩ ∼ G) |
103 | 101, 102 | eqtri 2373 |
. . . . . . 7
⊢ D = (ran R ∩
∼ G) |
104 | 100, 68, 103 | 3sstr4g 3312 |
. . . . . 6
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
B ⊆
D) |
105 | | ssdif 3401 |
. . . . . . . 8
⊢ (ran R ⊆ X → (ran R
∖ G)
⊆ (X
∖ G)) |
106 | 45, 105 | syl 15 |
. . . . . . 7
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(ran R ∖
G) ⊆
(X ∖
G)) |
107 | 106, 101,
68 | 3sstr4g 3312 |
. . . . . 6
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
D ⊆
B) |
108 | 104, 107 | eqssd 3289 |
. . . . 5
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
B = D) |
109 | 71, 108 | syl5breq 4674 |
. . . 4
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
B ≈ D) |
110 | 10, 68 | ineq12i 3455 |
. . . . . 6
⊢ (A ∩ B) =
((X ∩ G) ∩ (X
∖ G)) |
111 | | inindif 4075 |
. . . . . 6
⊢ ((X ∩ G) ∩
(X ∖
G)) = ∅ |
112 | 110, 111 | eqtri 2373 |
. . . . 5
⊢ (A ∩ B) =
∅ |
113 | 30, 101 | ineq12i 3455 |
. . . . . 6
⊢ (C ∩ D) =
((ran R ∩ G) ∩ (ran R
∖ G)) |
114 | | inindif 4075 |
. . . . . 6
⊢ ((ran R ∩ G) ∩
(ran R ∖
G)) = ∅ |
115 | 113, 114 | eqtri 2373 |
. . . . 5
⊢ (C ∩ D) =
∅ |
116 | | unen 6048 |
. . . . 5
⊢ (((A ≈ C
∧ B
≈ D) ∧ ((A ∩
B) = ∅
∧ (C ∩
D) = ∅))
→ (A ∪ B) ≈ (C
∪ D)) |
117 | 112, 115,
116 | mpanr12 666 |
. . . 4
⊢ ((A ≈ C
∧ B
≈ D) → (A ∪ B)
≈ (C ∪ D)) |
118 | 67, 109, 117 | syl2anc 642 |
. . 3
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(A ∪ B) ≈ (C
∪ D)) |
119 | | ensym 6037 |
. . 3
⊢ ((A ∪ B)
≈ (C ∪ D) ↔ (C
∪ D) ≈ (A ∪ B)) |
120 | 118, 119 | sylib 188 |
. 2
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
(C ∪ D) ≈ (A
∪ B)) |
121 | 30, 101 | uneq12i 3416 |
. . 3
⊢ (C ∪ D) =
((ran R ∩ G) ∪ (ran R
∖ G)) |
122 | | inundif 3628 |
. . 3
⊢ ((ran R ∩ G) ∪
(ran R ∖
G)) = ran R |
123 | 121, 122 | eqtri 2373 |
. 2
⊢ (C ∪ D) = ran
R |
124 | 10, 68 | uneq12i 3416 |
. . 3
⊢ (A ∪ B) =
((X ∩ G) ∪ (X
∖ G)) |
125 | | inundif 3628 |
. . 3
⊢ ((X ∩ G) ∪
(X ∖
G)) = X |
126 | 124, 125 | eqtri 2373 |
. 2
⊢ (A ∪ B) =
X |
127 | 120, 123,
126 | 3brtr3g 4670 |
1
⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) →
ran R ≈ X) |