Step | Hyp | Ref
| Expression |
1 | | df-sfin 4446 |
. . 3
⊢ ( Sfin (M,
N) ↔ (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N))) |
2 | | df-sfin 4446 |
. . 3
⊢ ( Sfin (P,
Q) ↔ (P ∈ Nn ∧ Q ∈ Nn ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q))) |
3 | | 3an6 1262 |
. . . 4
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ (∃a(℘1a ∈ M ∧ ℘a ∈ N) ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q))) ↔
((M ∈
Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)) ∧ (P ∈ Nn ∧ Q ∈ Nn ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q)))) |
4 | | eeanv 1913 |
. . . . . 6
⊢ (∃a∃b((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q)) ↔
(∃a(℘1a ∈ M ∧ ℘a ∈ N) ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q))) |
5 | | simp1l 979 |
. . . . . . . . . 10
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
M ∈ Nn ) |
6 | | simp3ll 1026 |
. . . . . . . . . 10
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
℘1a ∈ M) |
7 | | ncfinlower 4483 |
. . . . . . . . . 10
⊢ ((M ∈ Nn ∧ ℘1a ∈ M ∧ ℘1a ∈ M) → ∃r ∈ Nn (a ∈ r ∧ a ∈ r)) |
8 | 5, 6, 6, 7 | syl3anc 1182 |
. . . . . . . . 9
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
∃r ∈ Nn (a ∈ r ∧ a ∈ r)) |
9 | | simp1r 980 |
. . . . . . . . . 10
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
P ∈ Nn ) |
10 | | simp3rl 1028 |
. . . . . . . . . 10
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
℘1b ∈ P) |
11 | | ncfinlower 4483 |
. . . . . . . . . 10
⊢ ((P ∈ Nn ∧ ℘1b ∈ P ∧ ℘1b ∈ P) → ∃s ∈ Nn (b ∈ s ∧ b ∈ s)) |
12 | 9, 10, 10, 11 | syl3anc 1182 |
. . . . . . . . 9
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
∃s ∈ Nn (b ∈ s ∧ b ∈ s)) |
13 | | reeanv 2778 |
. . . . . . . . . 10
⊢ (∃r ∈ Nn ∃s ∈ Nn ((a ∈ r ∧ a ∈ r) ∧ (b ∈ s ∧ b ∈ s)) ↔ (∃r ∈ Nn (a ∈ r ∧ a ∈ r) ∧ ∃s ∈ Nn (b ∈ s ∧ b ∈ s))) |
14 | | simpl 443 |
. . . . . . . . . . . . 13
⊢ ((a ∈ r ∧ a ∈ r) → a
∈ r) |
15 | | simpl 443 |
. . . . . . . . . . . . 13
⊢ ((b ∈ s ∧ b ∈ s) → b
∈ s) |
16 | 14, 15 | anim12i 549 |
. . . . . . . . . . . 12
⊢ (((a ∈ r ∧ a ∈ r) ∧ (b ∈ s ∧ b ∈ s)) → (a
∈ r ∧ b ∈ s)) |
17 | 6 | adantr 451 |
. . . . . . . . . . . . . . . . 17
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
℘1a ∈ M) |
18 | | simprll 738 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
r ∈ Nn ) |
19 | | simprrl 740 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
a ∈
r) |
20 | | tfinpw1 4494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((r ∈ Nn ∧ a ∈ r) → ℘1a ∈ Tfin r) |
21 | 18, 19, 20 | syl2anc 642 |
. . . . . . . . . . . . . . . . 17
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
℘1a ∈ Tfin r) |
22 | | elin 3219 |
. . . . . . . . . . . . . . . . 17
⊢ (℘1a ∈ (M ∩ Tfin
r) ↔ (℘1a ∈ M ∧ ℘1a ∈ Tfin r)) |
23 | 17, 21, 22 | sylanbrc 645 |
. . . . . . . . . . . . . . . 16
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
℘1a ∈ (M ∩ Tfin
r)) |
24 | | n0i 3555 |
. . . . . . . . . . . . . . . 16
⊢ (℘1a ∈ (M ∩ Tfin
r) → ¬ (M ∩ Tfin
r) = ∅) |
25 | 23, 24 | syl 15 |
. . . . . . . . . . . . . . 15
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
¬ (M ∩ Tfin r) =
∅) |
26 | | simpl1l 1006 |
. . . . . . . . . . . . . . . 16
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
M ∈ Nn ) |
27 | | ne0i 3556 |
. . . . . . . . . . . . . . . . . 18
⊢ (a ∈ r → r ≠
∅) |
28 | 19, 27 | syl 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
r ≠ ∅) |
29 | | tfinprop 4489 |
. . . . . . . . . . . . . . . . . 18
⊢ ((r ∈ Nn ∧ r ≠ ∅) →
( Tfin r ∈ Nn ∧ ∃a ∈ r ℘1a ∈ Tfin r)) |
30 | 29 | simpld 445 |
. . . . . . . . . . . . . . . . 17
⊢ ((r ∈ Nn ∧ r ≠ ∅) →
Tfin r ∈ Nn ) |
31 | 18, 28, 30 | syl2anc 642 |
. . . . . . . . . . . . . . . 16
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
Tfin r ∈ Nn ) |
32 | | nndisjeq 4429 |
. . . . . . . . . . . . . . . 16
⊢ ((M ∈ Nn ∧ Tfin r
∈ Nn ) →
((M ∩ Tfin r) =
∅ ∨
M = Tfin r)) |
33 | 26, 31, 32 | syl2anc 642 |
. . . . . . . . . . . . . . 15
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
((M ∩ Tfin r) =
∅ ∨
M = Tfin r)) |
34 | | orel1 371 |
. . . . . . . . . . . . . . 15
⊢ (¬ (M ∩ Tfin
r) = ∅
→ (((M ∩ Tfin r) =
∅ ∨
M = Tfin r)
→ M = Tfin r)) |
35 | 25, 33, 34 | sylc 56 |
. . . . . . . . . . . . . 14
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
M = Tfin r) |
36 | 10 | adantr 451 |
. . . . . . . . . . . . . . . . 17
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
℘1b ∈ P) |
37 | | simprlr 739 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
s ∈ Nn ) |
38 | | simprrr 741 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
b ∈
s) |
39 | | tfinpw1 4494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((s ∈ Nn ∧ b ∈ s) → ℘1b ∈ Tfin s) |
40 | 37, 38, 39 | syl2anc 642 |
. . . . . . . . . . . . . . . . 17
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
℘1b ∈ Tfin s) |
41 | | elin 3219 |
. . . . . . . . . . . . . . . . 17
⊢ (℘1b ∈ (P ∩ Tfin
s) ↔ (℘1b ∈ P ∧ ℘1b ∈ Tfin s)) |
42 | 36, 40, 41 | sylanbrc 645 |
. . . . . . . . . . . . . . . 16
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
℘1b ∈ (P ∩ Tfin
s)) |
43 | | n0i 3555 |
. . . . . . . . . . . . . . . 16
⊢ (℘1b ∈ (P ∩ Tfin
s) → ¬ (P ∩ Tfin
s) = ∅) |
44 | 42, 43 | syl 15 |
. . . . . . . . . . . . . . 15
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
¬ (P ∩ Tfin s) =
∅) |
45 | | simpl1r 1007 |
. . . . . . . . . . . . . . . 16
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
P ∈ Nn ) |
46 | | ne0i 3556 |
. . . . . . . . . . . . . . . . . 18
⊢ (b ∈ s → s ≠
∅) |
47 | 38, 46 | syl 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
s ≠ ∅) |
48 | | tfinprop 4489 |
. . . . . . . . . . . . . . . . . 18
⊢ ((s ∈ Nn ∧ s ≠ ∅) →
( Tfin s ∈ Nn ∧ ∃a ∈ s ℘1a ∈ Tfin s)) |
49 | 48 | simpld 445 |
. . . . . . . . . . . . . . . . 17
⊢ ((s ∈ Nn ∧ s ≠ ∅) →
Tfin s ∈ Nn ) |
50 | 37, 47, 49 | syl2anc 642 |
. . . . . . . . . . . . . . . 16
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
Tfin s ∈ Nn ) |
51 | | nndisjeq 4429 |
. . . . . . . . . . . . . . . 16
⊢ ((P ∈ Nn ∧ Tfin s
∈ Nn ) →
((P ∩ Tfin s) =
∅ ∨
P = Tfin s)) |
52 | 45, 50, 51 | syl2anc 642 |
. . . . . . . . . . . . . . 15
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
((P ∩ Tfin s) =
∅ ∨
P = Tfin s)) |
53 | | orel1 371 |
. . . . . . . . . . . . . . 15
⊢ (¬ (P ∩ Tfin
s) = ∅
→ (((P ∩ Tfin s) =
∅ ∨
P = Tfin s)
→ P = Tfin s)) |
54 | 44, 52, 53 | sylc 56 |
. . . . . . . . . . . . . 14
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
P = Tfin s) |
55 | | tfinltfin 4501 |
. . . . . . . . . . . . . . . . 17
⊢ ((r ∈ Nn ∧ s ∈ Nn ) → (⟪r, s⟫
∈ <fin ↔ ⟪ Tfin r,
Tfin s⟫ ∈
<fin )) |
56 | 55 | ad2antrl 708 |
. . . . . . . . . . . . . . . 16
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
(⟪r, s⟫ ∈
<fin ↔ ⟪ Tfin
r, Tfin s⟫ ∈
<fin )) |
57 | | opkltfing 4449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((r ∈ Nn ∧ s ∈ Nn ) → (⟪r, s⟫
∈ <fin ↔ (r ≠ ∅ ∧ ∃t ∈ Nn s = ((r +c t) +c
1c)))) |
58 | 57 | ad2antrl 708 |
. . . . . . . . . . . . . . . . 17
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
(⟪r, s⟫ ∈
<fin ↔ (r ≠ ∅ ∧ ∃t ∈ Nn s = ((r
+c t)
+c 1c)))) |
59 | | simp2rr 1025 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ b ∈ s) |
60 | | simp3r 984 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ s = ((r +c t) +c
1c)) |
61 | 59, 60 | eleqtrd 2429 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ b ∈ ((r
+c t)
+c 1c)) |
62 | | addcass 4415 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((r +c t) +c 1c) =
(r +c (t +c
1c)) |
63 | 61, 62 | syl6eleq 2443 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ b ∈ (r
+c (t
+c 1c))) |
64 | | eladdc 4398 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (b ∈ (r +c (t +c 1c)) ↔
∃g ∈ r ∃d ∈ (t
+c 1c)((g ∩ d) =
∅ ∧
b = (g
∪ d))) |
65 | | 0nelsuc 4400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ¬ ∅ ∈ (t +c
1c) |
66 | | simprlr 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ d ∈ (t
+c 1c)) |
67 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (d = ∅ →
(d ∈
(t +c
1c) ↔ ∅ ∈ (t
+c 1c))) |
68 | 66, 67 | syl5ibcom 211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ (d = ∅ → ∅
∈ (t
+c 1c))) |
69 | 65, 68 | mtoi 169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ ¬ d = ∅) |
70 | | df-ne 2518 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (d ≠ ∅ ↔
¬ d = ∅) |
71 | 69, 70 | sylibr 203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ d ≠ ∅) |
72 | | n0 3559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (d ≠ ∅ ↔
∃x
x ∈
d) |
73 | | ssun2 3427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ d ⊆ (g ∪ d) |
74 | | sseq2 3293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (b = (g ∪
d) → (d ⊆ b ↔ d ⊆ (g ∪
d))) |
75 | 73, 74 | mpbiri 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (b = (g ∪
d) → d ⊆ b) |
76 | 75 | sseld 3272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (b = (g ∪
d) → (x ∈ d → x ∈ b)) |
77 | | disjr 3592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((g ∩ d) =
∅ ↔ ∀x ∈ d ¬
x ∈
g) |
78 | | rsp 2674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (∀x ∈ d ¬
x ∈
g → (x ∈ d → ¬ x
∈ g)) |
79 | 77, 78 | sylbi 187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((g ∩ d) =
∅ → (x ∈ d → ¬ x
∈ g)) |
80 | 76, 79 | anim12ii 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((b = (g ∪
d) ∧
(g ∩ d) = ∅) →
(x ∈
d → (x ∈ b ∧ ¬ x ∈ g))) |
81 | 80 | ancoms 439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((g ∩ d) =
∅ ∧
b = (g
∪ d)) → (x ∈ d → (x
∈ b ∧ ¬ x ∈ g))) |
82 | 81 | ad2antll 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ (x ∈ d →
(x ∈
b ∧ ¬
x ∈
g))) |
83 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ x ∈
V |
84 | 83 | snelpw 4115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ({x} ∈ ℘b ↔
x ∈
b) |
85 | 83 | snelpw 4115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ({x} ∈ ℘g ↔
x ∈
g) |
86 | 85 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (¬ {x} ∈ ℘g ↔
¬ x ∈
g) |
87 | 84, 86 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (({x} ∈ ℘b ∧ ¬ {x}
∈ ℘g) ↔
(x ∈
b ∧ ¬
x ∈
g)) |
88 | | ssun1 3426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ g ⊆ (g ∪ d) |
89 | | sseq2 3293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (b = (g ∪
d) → (g ⊆ b ↔ g ⊆ (g ∪
d))) |
90 | 88, 89 | mpbiri 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (b = (g ∪
d) → g ⊆ b) |
91 | | sspwb 4118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (g ⊆ b ↔ ℘g ⊆ ℘b) |
92 | 90, 91 | sylib 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (b = (g ∪
d) → ℘g ⊆ ℘b) |
93 | 92 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((g ∩ d) =
∅ ∧
b = (g
∪ d)) → ℘g ⊆ ℘b) |
94 | 93 | ad2antll 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ ℘g ⊆ ℘b) |
95 | | eleq2 2414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (℘g = ℘b →
({x} ∈
℘g
↔ {x} ∈ ℘b)) |
96 | 95 | biimprcd 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ({x} ∈ ℘b →
(℘g =
℘b
→ {x} ∈ ℘g)) |
97 | 96 | con3d 125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ({x} ∈ ℘b →
(¬ {x} ∈ ℘g → ¬ ℘g = ℘b)) |
98 | 97 | imp 418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (({x} ∈ ℘b ∧ ¬ {x}
∈ ℘g) →
¬ ℘g = ℘b) |
99 | 98 | anim2i 552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((℘g ⊆ ℘b ∧ ({x} ∈ ℘b ∧ ¬ {x}
∈ ℘g)) →
(℘g
⊆ ℘b ∧ ¬ ℘g = ℘b)) |
100 | | dfpss2 3354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (℘g ⊊
℘b
↔ (℘g ⊆ ℘b ∧ ¬ ℘g = ℘b)) |
101 | 99, 100 | sylibr 203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((℘g ⊆ ℘b ∧ ({x} ∈ ℘b ∧ ¬ {x}
∈ ℘g)) →
℘g
⊊ ℘b) |
102 | | simp2ll 1022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ r ∈ Nn
) |
103 | 102 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ r ∈ Nn
) |
104 | | simp2rl 1024 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ a ∈ r) |
105 | 104 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ a ∈ r) |
106 | | simprll 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ g ∈ r) |
107 | | nnpweq 4523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((r ∈ Nn ∧ a ∈ r ∧ g ∈ r) → ∃u ∈ Nn (℘a ∈ u ∧ ℘g ∈ u)) |
108 | 103, 105,
106, 107 | syl3anc 1182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ ∃u ∈ Nn (℘a ∈ u ∧ ℘g ∈ u)) |
109 | | simpr2l 1014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
℘a
∈ u) |
110 | | simp3lr 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
℘a
∈ N) |
111 | 110 | 3ad2ant1 976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ ℘a ∈ N) |
112 | 111 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
℘a
∈ N) |
113 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (℘a ∈ (u ∩
N) ↔ (℘a ∈ u ∧ ℘a ∈ N)) |
114 | 109, 112,
113 | sylanbrc 645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
℘a
∈ (u
∩ N)) |
115 | | n0i 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (℘a ∈ (u ∩
N) → ¬ (u ∩ N) =
∅) |
116 | 114, 115 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
¬ (u ∩ N) = ∅) |
117 | | simpr1 961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
u ∈ Nn ) |
118 | | simp12l 1068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ N ∈ Nn
) |
119 | 118 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
N ∈ Nn ) |
120 | | nndisjeq 4429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((u ∈ Nn ∧ N ∈ Nn ) → ((u
∩ N) = ∅ ∨ u = N)) |
121 | 117, 119,
120 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
((u ∩ N) = ∅ ∨ u = N)) |
122 | | orel1 371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (¬ (u ∩ N) =
∅ → (((u ∩ N) =
∅ ∨
u = N)
→ u = N)) |
123 | 116, 121,
122 | sylc 56 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
u = N) |
124 | | simp3rr 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
℘b
∈ Q) |
125 | 124 | 3ad2ant1 976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ ℘b ∈ Q) |
126 | 125 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
℘b
∈ Q) |
127 | | simp12r 1069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ Q ∈ Nn
) |
128 | 127 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
Q ∈ Nn ) |
129 | | elunii 3896 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((℘b ∈ Q ∧ Q ∈ Nn ) → ℘b ∈ ∪ Nn ) |
130 | 126, 128,
129 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
℘b
∈ ∪ Nn ) |
131 | | df-fin 4380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ Fin = ∪ Nn |
132 | 130, 131 | syl6eleqr 2444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
℘b
∈ Fin
) |
133 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ b ∈
V |
134 | 133 | pwex 4329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ℘b ∈ V |
135 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ g ∈
V |
136 | 135 | pwex 4329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ℘g ∈ V |
137 | 134, 136 | difex 4107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (℘b ∖ ℘g) ∈
V |
138 | | difss 3393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (℘b ∖ ℘g) ⊆ ℘b |
139 | | ssfin 4470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((℘b ∖ ℘g) ∈ V ∧ ℘b ∈ Fin ∧ (℘b ∖ ℘g) ⊆ ℘b) →
(℘b
∖ ℘g) ∈ Fin
) |
140 | 137, 138,
139 | mp3an13 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (℘b ∈ Fin → (℘b ∖ ℘g) ∈ Fin ) |
141 | 132, 140 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
(℘b
∖ ℘g) ∈ Fin
) |
142 | | elfin 4420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((℘b ∖ ℘g) ∈ Fin ↔ ∃n ∈ Nn (℘b ∖ ℘g) ∈ n) |
143 | 125 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ ℘b ∈ Q) |
144 | 143 | 3ad2ant1 976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
℘b
∈ Q) |
145 | | undif1 3625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((℘b ∖ ℘g) ∪ ℘g) = (℘b ∪
℘g) |
146 | | uncom 3408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((℘b ∖ ℘g) ∪ ℘g) = (℘g ∪
(℘b
∖ ℘g)) |
147 | 145, 146 | eqtr3i 2375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (℘b ∪
℘g) =
(℘g
∪ (℘b ∖ ℘g)) |
148 | | simp23 990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
℘g
⊊ ℘b) |
149 | 148 | pssssd 3366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
℘g
⊆ ℘b) |
150 | | ssequn2 3436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (℘g ⊆ ℘b ↔ (℘b ∪
℘g) =
℘b) |
151 | 149, 150 | sylib 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
(℘b
∪ ℘g) = ℘b) |
152 | 147, 151 | syl5eqr 2399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
(℘g
∪ (℘b ∖ ℘g)) = ℘b) |
153 | | simp22r 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
℘g
∈ u) |
154 | | simp3r 984 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
(℘b
∖ ℘g) ∈ n) |
155 | | disjdif 3622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (℘g ∩
(℘b
∖ ℘g)) = ∅ |
156 | 155 | a1i 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
(℘g
∩ (℘b ∖ ℘g)) = ∅) |
157 | | eladdci 4399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((℘g ∈ u ∧ (℘b ∖ ℘g) ∈ n ∧ (℘g ∩ (℘b ∖ ℘g)) = ∅) →
(℘g
∪ (℘b ∖ ℘g)) ∈ (u
+c n)) |
158 | 153, 154,
156, 157 | syl3anc 1182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
(℘g
∪ (℘b ∖ ℘g)) ∈ (u
+c n)) |
159 | 152, 158 | eqeltrrd 2428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
℘b
∈ (u
+c n)) |
160 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (℘b ∈ (Q ∩
(u +c n)) ↔ (℘b ∈ Q ∧ ℘b ∈ (u +c n))) |
161 | 144, 159,
160 | sylanbrc 645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
℘b
∈ (Q
∩ (u +c n))) |
162 | | n0i 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (℘b ∈ (Q ∩
(u +c n)) → ¬ (Q ∩ (u
+c n)) = ∅) |
163 | 161, 162 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
¬ (Q ∩ (u +c n)) = ∅) |
164 | 127 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ Q ∈ Nn
) |
165 | 164 | 3ad2ant1 976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
Q ∈ Nn ) |
166 | | simp21 988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
u ∈ Nn ) |
167 | | simp3l 983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
n ∈ Nn ) |
168 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((u ∈ Nn ∧ n ∈ Nn ) → (u
+c n) ∈ Nn
) |
169 | 166, 167,
168 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
(u +c n) ∈ Nn ) |
170 | | nndisjeq 4429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((Q ∈ Nn ∧ (u +c n) ∈ Nn ) → ((Q
∩ (u +c n)) = ∅ ∨ Q = (u +c n))) |
171 | 165, 169,
170 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
((Q ∩ (u +c n)) = ∅ ∨ Q = (u +c n))) |
172 | | orel1 371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (¬ (Q ∩ (u
+c n)) = ∅ → (((Q
∩ (u +c n)) = ∅ ∨ Q = (u +c n)) → Q =
(u +c n))) |
173 | 163, 171,
172 | sylc 56 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
Q = (u
+c n)) |
174 | | ne0i 3556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (℘g ∈ u →
u ≠ ∅) |
175 | 153, 174 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
u ≠ ∅) |
176 | | df-pss 3261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (℘g ⊊
℘b
↔ (℘g ⊆ ℘b ∧ ℘g ≠ ℘b)) |
177 | | ssdif0 3609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ (℘b ⊆ ℘g ↔ (℘b ∖ ℘g) = ∅) |
178 | | eqss 3287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ (℘g = ℘b ↔
(℘g
⊆ ℘b ∧ ℘b ⊆ ℘g)) |
179 | 178 | simplbi2 608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ (℘g ⊆ ℘b → (℘b ⊆ ℘g → ℘g = ℘b)) |
180 | 177, 179 | syl5bir 209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (℘g ⊆ ℘b → ((℘b ∖ ℘g) = ∅ →
℘g =
℘b)) |
181 | 180 | necon3d 2554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (℘g ⊆ ℘b → (℘g ≠ ℘b →
(℘b
∖ ℘g) ≠
∅)) |
182 | 181 | imp 418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((℘g ⊆ ℘b ∧ ℘g ≠ ℘b) →
(℘b
∖ ℘g) ≠
∅) |
183 | 176, 182 | sylbi 187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (℘g ⊊
℘b
→ (℘b ∖ ℘g) ≠
∅) |
184 | 148, 183 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
(℘b
∖ ℘g) ≠
∅) |
185 | | eleq2 2414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (n = 0c → ((℘b ∖ ℘g) ∈ n ↔ (℘b ∖ ℘g) ∈
0c)) |
186 | 185 | biimpcd 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((℘b ∖ ℘g) ∈ n → (n =
0c → (℘b ∖ ℘g) ∈ 0c)) |
187 | | el0c 4421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((℘b ∖ ℘g) ∈
0c ↔ (℘b ∖ ℘g) = ∅) |
188 | 186, 187 | syl6ib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((℘b ∖ ℘g) ∈ n → (n =
0c → (℘b ∖ ℘g) = ∅)) |
189 | 188 | necon3ad 2552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((℘b ∖ ℘g) ∈ n → ((℘b ∖ ℘g) ≠ ∅ →
¬ n =
0c)) |
190 | 154, 184,
189 | sylc 56 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
¬ n =
0c) |
191 | | nnc0suc 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (n ∈ Nn ↔ (n =
0c ∨ ∃m ∈ Nn n = (m
+c 1c))) |
192 | 167, 191 | sylib 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
(n = 0c ∨ ∃m ∈ Nn n = (m +c
1c))) |
193 | | orel1 371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (¬ n = 0c → ((n = 0c
∨ ∃m ∈ Nn n = (m +c 1c)) →
∃m ∈ Nn n = (m
+c 1c))) |
194 | 190, 192,
193 | sylc 56 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
∃m ∈ Nn n = (m
+c 1c)) |
195 | | addceq2 4384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (n = (m
+c 1c) → (u +c n) = (u
+c (m
+c 1c))) |
196 | | addcass 4415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((u +c m) +c 1c) =
(u +c (m +c
1c)) |
197 | 195, 196 | syl6eqr 2403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (n = (m
+c 1c) → (u +c n) = ((u
+c m)
+c 1c)) |
198 | 197 | reximi 2721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (∃m ∈ Nn n = (m
+c 1c) → ∃m ∈ Nn (u +c n) = ((u
+c m)
+c 1c)) |
199 | 194, 198 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
∃m ∈ Nn (u +c n) = ((u
+c m)
+c 1c)) |
200 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ u ∈
V |
201 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ n ∈
V |
202 | 200, 201 | addcex 4394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (u +c n) ∈
V |
203 | | opkltfing 4449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((u ∈ V ∧ (u
+c n) ∈ V) → (⟪u, (u
+c n)⟫ ∈ <fin ↔ (u ≠ ∅ ∧ ∃m ∈ Nn (u
+c n) = ((u +c m) +c
1c)))) |
204 | 200, 202,
203 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (⟪u, (u
+c n)⟫ ∈ <fin ↔ (u ≠ ∅ ∧ ∃m ∈ Nn (u
+c n) = ((u +c m) +c
1c))) |
205 | 175, 199,
204 | sylanbrc 645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
⟪u, (u +c n)⟫ ∈
<fin ) |
206 | | opkeq2 4060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (Q = (u
+c n) →
⟪u, Q⟫ = ⟪u, (u
+c n)⟫) |
207 | 206 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (Q = (u
+c n) →
(⟪u, Q⟫ ∈
<fin ↔ ⟪u,
(u +c n)⟫ ∈
<fin )) |
208 | 205, 207 | syl5ibrcom 213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
(Q = (u
+c n) →
⟪u, Q⟫ ∈
<fin )) |
209 | 173, 208 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
⟪u, Q⟫ ∈
<fin ) |
210 | 209 | 3expa 1151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) ∧ (n ∈ Nn ∧ (℘b ∖ ℘g) ∈ n)) →
⟪u, Q⟫ ∈
<fin ) |
211 | 210 | exp32 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
(n ∈
Nn → ((℘b ∖ ℘g) ∈ n → ⟪u, Q⟫
∈ <fin ))) |
212 | 211 | rexlimdv 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
(∃n
∈ Nn (℘b ∖ ℘g) ∈ n → ⟪u, Q⟫
∈ <fin )) |
213 | 142, 212 | syl5bi 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
((℘b
∖ ℘g) ∈ Fin →
⟪u, Q⟫ ∈
<fin )) |
214 | 141, 213 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
⟪u, Q⟫ ∈
<fin ) |
215 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (u = N →
⟪u, Q⟫ = ⟪N, Q⟫) |
216 | 215 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (u = N →
(⟪u, Q⟫ ∈
<fin ↔ ⟪N,
Q⟫ ∈ <fin )) |
217 | 214, 216 | syl5ibcom 211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
(u = N
→ ⟪N, Q⟫ ∈
<fin )) |
218 | 123, 217 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
∧ (u ∈ Nn ∧ (℘a ∈ u ∧ ℘g ∈ u) ∧ ℘g ⊊ ℘b)) →
⟪N, Q⟫ ∈
<fin ) |
219 | 218 | 3exp2 1169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ (u ∈ Nn → ((℘a ∈ u ∧ ℘g ∈ u) → (℘g ⊊
℘b
→ ⟪N, Q⟫ ∈
<fin )))) |
220 | 219 | rexlimdv 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ (∃u ∈ Nn (℘a ∈ u ∧ ℘g ∈ u) →
(℘g
⊊ ℘b → ⟪N, Q⟫
∈ <fin ))) |
221 | 108, 220 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ (℘g ⊊ ℘b →
⟪N, Q⟫ ∈
<fin )) |
222 | 101, 221 | syl5 28 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ ((℘g ⊆ ℘b ∧ ({x} ∈ ℘b ∧ ¬ {x} ∈ ℘g)) →
⟪N, Q⟫ ∈
<fin )) |
223 | 94, 222 | mpand 656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ (({x} ∈ ℘b ∧ ¬ {x} ∈ ℘g) →
⟪N, Q⟫ ∈
<fin )) |
224 | 87, 223 | syl5bir 209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ ((x ∈ b ∧ ¬ x ∈ g) →
⟪N, Q⟫ ∈
<fin )) |
225 | 82, 224 | syld 40 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ (x ∈ d →
⟪N, Q⟫ ∈
<fin )) |
226 | 225 | exlimdv 1636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ (∃x x ∈ d →
⟪N, Q⟫ ∈
<fin )) |
227 | 72, 226 | syl5bi 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ (d ≠ ∅ → ⟪N, Q⟫
∈ <fin )) |
228 | 71, 227 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
∧ ((g
∈ r ∧ d ∈ (t
+c 1c)) ∧
((g ∩ d) = ∅ ∧ b = (g ∪ d))))
→ ⟪N, Q⟫ ∈
<fin ) |
229 | 228 | exp32 588 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ ((g ∈ r ∧ d ∈ (t
+c 1c)) → (((g ∩ d) =
∅ ∧
b = (g
∪ d)) → ⟪N, Q⟫
∈ <fin ))) |
230 | 229 | rexlimdvv 2744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ (∃g ∈ r ∃d ∈ (t +c
1c)((g ∩ d) = ∅ ∧ b = (g ∪ d))
→ ⟪N, Q⟫ ∈
<fin )) |
231 | 64, 230 | syl5bi 208 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ (b ∈ (r
+c (t
+c 1c)) → ⟪N, Q⟫
∈ <fin )) |
232 | 63, 231 | mpd 14 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s)) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ ⟪N, Q⟫ ∈
<fin ) |
233 | 232 | 3expa 1151 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) ∧ (t ∈ Nn ∧ s = ((r +c t) +c 1c)))
→ ⟪N, Q⟫ ∈
<fin ) |
234 | 233 | exp32 588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
(t ∈
Nn → (s =
((r +c t) +c 1c) →
⟪N, Q⟫ ∈
<fin ))) |
235 | 234 | rexlimdv 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
(∃t
∈ Nn s = ((r
+c t)
+c 1c) → ⟪N, Q⟫
∈ <fin )) |
236 | 235 | adantld 453 |
. . . . . . . . . . . . . . . . 17
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
((r ≠ ∅ ∧ ∃t ∈ Nn s = ((r
+c t)
+c 1c)) → ⟪N, Q⟫
∈ <fin )) |
237 | 58, 236 | sylbid 206 |
. . . . . . . . . . . . . . . 16
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
(⟪r, s⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin )) |
238 | 56, 237 | sylbird 226 |
. . . . . . . . . . . . . . 15
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
(⟪ Tfin r, Tfin
s⟫ ∈ <fin → ⟪N, Q⟫
∈ <fin )) |
239 | | opkeq12 4061 |
. . . . . . . . . . . . . . . . 17
⊢ ((M = Tfin
r ∧
P = Tfin s)
→ ⟪M, P⟫ = ⟪ Tfin r,
Tfin s⟫) |
240 | 239 | eleq1d 2419 |
. . . . . . . . . . . . . . . 16
⊢ ((M = Tfin
r ∧
P = Tfin s)
→ (⟪M, P⟫ ∈
<fin ↔ ⟪ Tfin
r, Tfin s⟫ ∈
<fin )) |
241 | 240 | imbi1d 308 |
. . . . . . . . . . . . . . 15
⊢ ((M = Tfin
r ∧
P = Tfin s)
→ ((⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin ) ↔ (⟪ Tfin r,
Tfin s⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin ))) |
242 | 238, 241 | syl5ibrcom 213 |
. . . . . . . . . . . . . 14
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
((M = Tfin r
∧ P =
Tfin s) → (⟪M, P⟫
∈ <fin → ⟪N, Q⟫
∈ <fin ))) |
243 | 35, 54, 242 | mp2and 660 |
. . . . . . . . . . . . 13
⊢ ((((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) ∧ ((r ∈ Nn ∧ s ∈ Nn ) ∧ (a ∈ r ∧ b ∈ s))) →
(⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin )) |
244 | 243 | exp32 588 |
. . . . . . . . . . . 12
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
((r ∈
Nn ∧ s ∈ Nn ) → ((a
∈ r ∧ b ∈ s) →
(⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin )))) |
245 | 16, 244 | syl7 63 |
. . . . . . . . . . 11
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
((r ∈
Nn ∧ s ∈ Nn ) → (((a
∈ r ∧ a ∈ r) ∧ (b ∈ s ∧ b ∈ s)) →
(⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin )))) |
246 | 245 | rexlimdvv 2744 |
. . . . . . . . . 10
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
(∃r
∈ Nn ∃s ∈ Nn ((a ∈ r ∧ a ∈ r) ∧ (b ∈ s ∧ b ∈ s)) → (⟪M, P⟫
∈ <fin → ⟪N, Q⟫
∈ <fin ))) |
247 | 13, 246 | syl5bir 209 |
. . . . . . . . 9
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
((∃r
∈ Nn (a ∈ r ∧ a ∈ r) ∧ ∃s ∈ Nn (b ∈ s ∧ b ∈ s)) → (⟪M, P⟫
∈ <fin → ⟪N, Q⟫
∈ <fin ))) |
248 | 8, 12, 247 | mp2and 660 |
. . . . . . . 8
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ ((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q))) →
(⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin )) |
249 | 248 | 3expia 1153 |
. . . . . . 7
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn )) → (((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q)) →
(⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin ))) |
250 | 249 | exlimdvv 1637 |
. . . . . 6
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn )) → (∃a∃b((℘1a ∈ M ∧ ℘a ∈ N) ∧ (℘1b ∈ P ∧ ℘b ∈ Q)) →
(⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin ))) |
251 | 4, 250 | syl5bir 209 |
. . . . 5
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn )) → ((∃a(℘1a ∈ M ∧ ℘a ∈ N) ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q)) →
(⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin ))) |
252 | 251 | 3impia 1148 |
. . . 4
⊢ (((M ∈ Nn ∧ P ∈ Nn ) ∧ (N ∈ Nn ∧ Q ∈ Nn ) ∧ (∃a(℘1a ∈ M ∧ ℘a ∈ N) ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q))) →
(⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin )) |
253 | 3, 252 | sylbir 204 |
. . 3
⊢ (((M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)) ∧ (P ∈ Nn ∧ Q ∈ Nn ∧ ∃b(℘1b ∈ P ∧ ℘b ∈ Q))) →
(⟪M, P⟫ ∈
<fin → ⟪N,
Q⟫ ∈ <fin )) |
254 | 1, 2, 253 | syl2anb 465 |
. 2
⊢ (( Sfin (M,
N) ∧ Sfin (P,
Q)) → (⟪M, P⟫
∈ <fin → ⟪N, Q⟫
∈ <fin )) |
255 | 254 | imp 418 |
1
⊢ ((( Sfin (M,
N) ∧ Sfin (P,
Q)) ∧
⟪M, P⟫ ∈
<fin ) → ⟪N,
Q⟫ ∈ <fin ) |