Step | Hyp | Ref
| Expression |
1 | | tfineq 4488 |
. . . . . . . . . . 11
⊢ (x = n →
Tfin x = Tfin
n) |
2 | 1 | eqeq2d 2364 |
. . . . . . . . . 10
⊢ (x = n →
(w = Tfin x
↔ w = Tfin n)) |
3 | 2 | cbvrexv 2836 |
. . . . . . . . 9
⊢ (∃x ∈ Spfin
w = Tfin x
↔ ∃n ∈ Spfin w =
Tfin n) |
4 | | vfinspsslem1 4550 |
. . . . . . . . . . . . 13
⊢ (((V ∈ Fin ∧ Tfin
n ∈ Spfin ) ∧
(n ∈
Spfin ∧ Sfin
(z, Tfin n)))
→ ∃x ∈ Spfin z =
Tfin x) |
5 | 4 | expr 598 |
. . . . . . . . . . . 12
⊢ (((V ∈ Fin ∧ Tfin
n ∈ Spfin ) ∧
n ∈ Spfin ) → ( Sfin (z,
Tfin n) → ∃x ∈ Spfin
z = Tfin x)) |
6 | | eleq1 2413 |
. . . . . . . . . . . . . . 15
⊢ (w = Tfin
n → (w ∈ Spfin ↔ Tfin n
∈ Spfin )) |
7 | 6 | anbi2d 684 |
. . . . . . . . . . . . . 14
⊢ (w = Tfin
n → ((V ∈ Fin ∧ w ∈ Spfin )
↔ (V ∈ Fin
∧ Tfin
n ∈ Spfin ))) |
8 | 7 | anbi1d 685 |
. . . . . . . . . . . . 13
⊢ (w = Tfin
n → (((V ∈ Fin ∧ w ∈ Spfin )
∧ n ∈ Spfin )
↔ ((V ∈ Fin
∧ Tfin
n ∈ Spfin ) ∧
n ∈ Spfin ))) |
9 | | sfineq2 4527 |
. . . . . . . . . . . . . 14
⊢ (w = Tfin
n → ( Sfin (z,
w) ↔ Sfin (z,
Tfin n))) |
10 | 9 | imbi1d 308 |
. . . . . . . . . . . . 13
⊢ (w = Tfin
n → (( Sfin (z,
w) → ∃x ∈ Spfin
z = Tfin x)
↔ ( Sfin (z, Tfin
n) → ∃x ∈ Spfin
z = Tfin x))) |
11 | 8, 10 | imbi12d 311 |
. . . . . . . . . . . 12
⊢ (w = Tfin
n → ((((V ∈ Fin ∧ w ∈ Spfin )
∧ n ∈ Spfin )
→ ( Sfin (z, w) →
∃x ∈ Spfin
z = Tfin x))
↔ (((V ∈ Fin ∧ Tfin n
∈ Spfin ) ∧
n ∈ Spfin ) → ( Sfin (z,
Tfin n) → ∃x ∈ Spfin
z = Tfin x)))) |
12 | 5, 11 | mpbiri 224 |
. . . . . . . . . . 11
⊢ (w = Tfin
n → (((V ∈ Fin ∧ w ∈ Spfin )
∧ n ∈ Spfin )
→ ( Sfin (z, w) →
∃x ∈ Spfin
z = Tfin x))) |
13 | 12 | com12 27 |
. . . . . . . . . 10
⊢ (((V ∈ Fin ∧ w ∈ Spfin )
∧ n ∈ Spfin )
→ (w = Tfin n
→ ( Sfin (z, w) →
∃x ∈ Spfin
z = Tfin x))) |
14 | 13 | rexlimdva 2738 |
. . . . . . . . 9
⊢ ((V ∈ Fin ∧ w ∈ Spfin )
→ (∃n ∈ Spfin w =
Tfin n → ( Sfin (z,
w) → ∃x ∈ Spfin
z = Tfin x))) |
15 | 3, 14 | syl5bi 208 |
. . . . . . . 8
⊢ ((V ∈ Fin ∧ w ∈ Spfin )
→ (∃x ∈ Spfin w =
Tfin x → ( Sfin (z,
w) → ∃x ∈ Spfin
z = Tfin x))) |
16 | | sfineq2 4527 |
. . . . . . . . . . . 12
⊢ (w = Ncfin V
→ ( Sfin (z, w) ↔
Sfin (z, Ncfin
V))) |
17 | 16 | biimpa 470 |
. . . . . . . . . . 11
⊢ ((w = Ncfin V
∧ Sfin
(z, w))
→ Sfin (z, Ncfin
V)) |
18 | | 1cvsfin 4542 |
. . . . . . . . . . . 12
⊢ (V ∈ Fin → Sfin ( Ncfin 1c, Ncfin V)) |
19 | | sfin111 4536 |
. . . . . . . . . . . . 13
⊢ (( Sfin ( Ncfin 1c, Ncfin V) ∧
Sfin (z, Ncfin V))
→ Ncfin 1c =
z) |
20 | | tncveqnc1fin 4544 |
. . . . . . . . . . . . . . . 16
⊢ (V ∈ Fin → Tfin Ncfin V = Ncfin 1c) |
21 | 20 | eqcomd 2358 |
. . . . . . . . . . . . . . 15
⊢ (V ∈ Fin → Ncfin 1c = Tfin Ncfin V) |
22 | | ncvspfin 4538 |
. . . . . . . . . . . . . . . 16
⊢ Ncfin V ∈
Spfin |
23 | | tfineq 4488 |
. . . . . . . . . . . . . . . . . 18
⊢ (x = Ncfin V
→ Tfin x = Tfin
Ncfin V) |
24 | 23 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . 17
⊢ (x = Ncfin V
→ ( Ncfin 1c =
Tfin x ↔ Ncfin 1c = Tfin Ncfin V)) |
25 | 24 | rspcev 2955 |
. . . . . . . . . . . . . . . 16
⊢ (( Ncfin V ∈
Spfin ∧ Ncfin
1c = Tfin Ncfin V) → ∃x ∈ Spfin
Ncfin 1c = Tfin x) |
26 | 22, 25 | mpan 651 |
. . . . . . . . . . . . . . 15
⊢ ( Ncfin 1c = Tfin Ncfin V → ∃x ∈ Spfin
Ncfin 1c = Tfin x) |
27 | 21, 26 | syl 15 |
. . . . . . . . . . . . . 14
⊢ (V ∈ Fin → ∃x ∈ Spfin
Ncfin 1c = Tfin x) |
28 | | eqeq1 2359 |
. . . . . . . . . . . . . . . . 17
⊢ ( Ncfin 1c = z → ( Ncfin 1c = Tfin x
↔ z = Tfin x)) |
29 | 28 | rexbidv 2635 |
. . . . . . . . . . . . . . . 16
⊢ ( Ncfin 1c = z → (∃x ∈ Spfin
Ncfin 1c = Tfin x
↔ ∃x ∈ Spfin z =
Tfin x)) |
30 | 29 | biimpd 198 |
. . . . . . . . . . . . . . 15
⊢ ( Ncfin 1c = z → (∃x ∈ Spfin
Ncfin 1c = Tfin x
→ ∃x ∈ Spfin z =
Tfin x)) |
31 | 30 | com12 27 |
. . . . . . . . . . . . . 14
⊢ (∃x ∈ Spfin
Ncfin 1c = Tfin x
→ ( Ncfin 1c =
z → ∃x ∈ Spfin
z = Tfin x)) |
32 | 27, 31 | syl 15 |
. . . . . . . . . . . . 13
⊢ (V ∈ Fin → ( Ncfin 1c = z → ∃x ∈ Spfin
z = Tfin x)) |
33 | 19, 32 | syl5 28 |
. . . . . . . . . . . 12
⊢ (V ∈ Fin → (( Sfin ( Ncfin 1c, Ncfin V) ∧
Sfin (z, Ncfin V))
→ ∃x ∈ Spfin z =
Tfin x)) |
34 | 18, 33 | mpand 656 |
. . . . . . . . . . 11
⊢ (V ∈ Fin → ( Sfin (z,
Ncfin V) → ∃x ∈ Spfin
z = Tfin x)) |
35 | 17, 34 | syl5 28 |
. . . . . . . . . 10
⊢ (V ∈ Fin →
((w = Ncfin V ∧
Sfin (z, w)) →
∃x ∈ Spfin
z = Tfin x)) |
36 | 35 | exp3a 425 |
. . . . . . . . 9
⊢ (V ∈ Fin → (w = Ncfin V
→ ( Sfin (z, w) →
∃x ∈ Spfin
z = Tfin x))) |
37 | 36 | adantr 451 |
. . . . . . . 8
⊢ ((V ∈ Fin ∧ w ∈ Spfin )
→ (w = Ncfin V → ( Sfin (z,
w) → ∃x ∈ Spfin
z = Tfin x))) |
38 | 15, 37 | jaod 369 |
. . . . . . 7
⊢ ((V ∈ Fin ∧ w ∈ Spfin )
→ ((∃x ∈ Spfin w =
Tfin x ∨ w = Ncfin V)
→ ( Sfin (z, w) →
∃x ∈ Spfin
z = Tfin x))) |
39 | 38 | imp3a 420 |
. . . . . 6
⊢ ((V ∈ Fin ∧ w ∈ Spfin )
→ (((∃x ∈ Spfin w =
Tfin x ∨ w = Ncfin V)
∧ Sfin
(z, w))
→ ∃x ∈ Spfin z =
Tfin x)) |
40 | | elun 3220 |
. . . . . . . 8
⊢ (w ∈ ({a ∣ ∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) ↔ (w ∈ {a ∣ ∃x ∈ Spfin
a = Tfin x}
∨ w ∈ { Ncfin
V})) |
41 | | vex 2862 |
. . . . . . . . . 10
⊢ w ∈
V |
42 | | eqeq1 2359 |
. . . . . . . . . . 11
⊢ (a = w →
(a = Tfin x
↔ w = Tfin x)) |
43 | 42 | rexbidv 2635 |
. . . . . . . . . 10
⊢ (a = w →
(∃x
∈ Spfin a =
Tfin x ↔ ∃x ∈ Spfin
w = Tfin x)) |
44 | 41, 43 | elab 2985 |
. . . . . . . . 9
⊢ (w ∈ {a ∣ ∃x ∈ Spfin
a = Tfin x}
↔ ∃x ∈ Spfin w =
Tfin x) |
45 | 41 | elsnc 3756 |
. . . . . . . . 9
⊢ (w ∈ { Ncfin V} ↔ w = Ncfin
V) |
46 | 44, 45 | orbi12i 507 |
. . . . . . . 8
⊢ ((w ∈ {a ∣ ∃x ∈ Spfin
a = Tfin x}
∨ w ∈ { Ncfin
V}) ↔ (∃x ∈ Spfin w =
Tfin x ∨ w = Ncfin
V)) |
47 | 40, 46 | bitri 240 |
. . . . . . 7
⊢ (w ∈ ({a ∣ ∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) ↔ (∃x ∈ Spfin
w = Tfin x
∨ w =
Ncfin V)) |
48 | 47 | anbi1i 676 |
. . . . . 6
⊢ ((w ∈ ({a ∣ ∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) ∧ Sfin
(z, w))
↔ ((∃x ∈ Spfin w =
Tfin x ∨ w = Ncfin V)
∧ Sfin
(z, w))) |
49 | | vex 2862 |
. . . . . . 7
⊢ z ∈
V |
50 | | eqeq1 2359 |
. . . . . . . 8
⊢ (a = z →
(a = Tfin x
↔ z = Tfin x)) |
51 | 50 | rexbidv 2635 |
. . . . . . 7
⊢ (a = z →
(∃x
∈ Spfin a =
Tfin x ↔ ∃x ∈ Spfin
z = Tfin x)) |
52 | 49, 51 | elab 2985 |
. . . . . 6
⊢ (z ∈ {a ∣ ∃x ∈ Spfin
a = Tfin x}
↔ ∃x ∈ Spfin z =
Tfin x) |
53 | 39, 48, 52 | 3imtr4g 261 |
. . . . 5
⊢ ((V ∈ Fin ∧ w ∈ Spfin )
→ ((w ∈ ({a ∣ ∃x ∈ Spfin a =
Tfin x} ∪ { Ncfin V}) ∧
Sfin (z, w)) →
z ∈
{a ∣
∃x ∈ Spfin
a = Tfin x})) |
54 | | ssun1 3426 |
. . . . . 6
⊢ {a ∣ ∃x ∈ Spfin
a = Tfin x}
⊆ ({a
∣ ∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) |
55 | 54 | sseli 3269 |
. . . . 5
⊢ (z ∈ {a ∣ ∃x ∈ Spfin
a = Tfin x}
→ z ∈ ({a ∣ ∃x ∈ Spfin a =
Tfin x} ∪ { Ncfin V})) |
56 | 53, 55 | syl6 29 |
. . . 4
⊢ ((V ∈ Fin ∧ w ∈ Spfin )
→ ((w ∈ ({a ∣ ∃x ∈ Spfin a =
Tfin x} ∪ { Ncfin V}) ∧
Sfin (z, w)) →
z ∈
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}))) |
57 | 56 | alrimiv 1631 |
. . 3
⊢ ((V ∈ Fin ∧ w ∈ Spfin )
→ ∀z((w ∈ ({a ∣ ∃x ∈ Spfin a =
Tfin x} ∪ { Ncfin V}) ∧
Sfin (z, w)) →
z ∈
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}))) |
58 | 57 | ralrimiva 2697 |
. 2
⊢ (V ∈ Fin → ∀w ∈ Spfin
∀z((w ∈ ({a ∣ ∃x ∈ Spfin a =
Tfin x} ∪ { Ncfin V}) ∧
Sfin (z, w)) →
z ∈
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}))) |
59 | | vex 2862 |
. . . . . . . . 9
⊢ a ∈
V |
60 | 59 | elimak 4259 |
. . . . . . . 8
⊢ (a ∈ ((({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) “k ℘1 Spfin ) ↔ ∃t ∈ ℘1
Spfin ⟪t, a⟫
∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) |
61 | | df-rex 2620 |
. . . . . . . . 9
⊢ (∃t ∈ ℘1
Spfin ⟪t, a⟫
∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) ↔ ∃t(t ∈ ℘1 Spfin ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
62 | | elpw1 4144 |
. . . . . . . . . . . . 13
⊢ (t ∈ ℘1 Spfin ↔ ∃x ∈ Spfin
t = {x}) |
63 | 62 | anbi1i 676 |
. . . . . . . . . . . 12
⊢ ((t ∈ ℘1 Spfin ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) ↔ (∃x ∈ Spfin
t = {x}
∧ ⟪t, a⟫
∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
64 | | r19.41v 2764 |
. . . . . . . . . . . 12
⊢ (∃x ∈ Spfin
(t = {x} ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) ↔ (∃x ∈ Spfin
t = {x}
∧ ⟪t, a⟫
∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
65 | 63, 64 | bitr4i 243 |
. . . . . . . . . . 11
⊢ ((t ∈ ℘1 Spfin ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) ↔ ∃x ∈ Spfin
(t = {x} ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
66 | 65 | exbii 1582 |
. . . . . . . . . 10
⊢ (∃t(t ∈ ℘1 Spfin ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) ↔ ∃t∃x ∈ Spfin
(t = {x} ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
67 | | rexcom4 2878 |
. . . . . . . . . 10
⊢ (∃x ∈ Spfin
∃t(t = {x} ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) ↔ ∃t∃x ∈ Spfin
(t = {x} ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
68 | 66, 67 | bitr4i 243 |
. . . . . . . . 9
⊢ (∃t(t ∈ ℘1 Spfin ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) ↔ ∃x ∈ Spfin
∃t(t = {x} ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
69 | 61, 68 | bitri 240 |
. . . . . . . 8
⊢ (∃t ∈ ℘1
Spfin ⟪t, a⟫
∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) ↔ ∃x ∈ Spfin
∃t(t = {x} ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
70 | 60, 69 | bitri 240 |
. . . . . . 7
⊢ (a ∈ ((({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) “k ℘1 Spfin ) ↔ ∃x ∈ Spfin
∃t(t = {x} ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
71 | | snex 4111 |
. . . . . . . . . 10
⊢ {x} ∈
V |
72 | | opkeq1 4059 |
. . . . . . . . . . 11
⊢ (t = {x} →
⟪t, a⟫ = ⟪{x}, a⟫) |
73 | 72 | eleq1d 2419 |
. . . . . . . . . 10
⊢ (t = {x} →
(⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) ↔ ⟪{x}, a⟫
∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))))) |
74 | 71, 73 | ceqsexv 2894 |
. . . . . . . . 9
⊢ (∃t(t = {x} ∧ ⟪t,
a⟫ ∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) ↔ ⟪{x}, a⟫
∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) |
75 | | vex 2862 |
. . . . . . . . . 10
⊢ x ∈
V |
76 | 75, 59 | eqtfinrelk 4486 |
. . . . . . . . 9
⊢ (⟪{x}, a⟫
∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) ↔ a =
Tfin x) |
77 | 74, 76 | bitri 240 |
. . . . . . . 8
⊢ (∃t(t = {x} ∧ ⟪t,
a⟫ ∈ (({{∅}}
×k {∅}) ∪ (
∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) ↔ a =
Tfin x) |
78 | 77 | rexbii 2639 |
. . . . . . 7
⊢ (∃x ∈ Spfin
∃t(t = {x} ∧
⟪t, a⟫ ∈
(({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V)))) ↔ ∃x ∈ Spfin
a = Tfin x) |
79 | 70, 78 | bitri 240 |
. . . . . 6
⊢ (a ∈ ((({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) “k ℘1 Spfin ) ↔ ∃x ∈ Spfin
a = Tfin x) |
80 | 79 | abbi2i 2464 |
. . . . 5
⊢ ((({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) “k ℘1 Spfin ) = {a ∣ ∃x ∈ Spfin
a = Tfin x} |
81 | | tfinrelkex 4487 |
. . . . . 6
⊢ (({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) ∈
V |
82 | | spfinex 4537 |
. . . . . . 7
⊢ Spfin ∈
V |
83 | 82 | pw1ex 4303 |
. . . . . 6
⊢ ℘1 Spfin ∈
V |
84 | 81, 83 | imakex 4300 |
. . . . 5
⊢ ((({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ⊕
Ins3k Ik )
“k ℘11c))
“k ℘11c))
“k ℘1℘11c) ∖ ({{∅}}
×k V))) “k ℘1 Spfin ) ∈
V |
85 | 80, 84 | eqeltrri 2424 |
. . . 4
⊢ {a ∣ ∃x ∈ Spfin
a = Tfin x}
∈ V |
86 | | snex 4111 |
. . . 4
⊢ { Ncfin V} ∈
V |
87 | 85, 86 | unex 4106 |
. . 3
⊢ ({a ∣ ∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) ∈ V |
88 | | ssun2 3427 |
. . . 4
⊢ { Ncfin V} ⊆
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) |
89 | | ncfinex 4472 |
. . . . 5
⊢ Ncfin V ∈
V |
90 | 89 | snid 3760 |
. . . 4
⊢ Ncfin V ∈ {
Ncfin V} |
91 | 88, 90 | sselii 3270 |
. . 3
⊢ Ncfin V ∈
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) |
92 | | spfininduct 4540 |
. . 3
⊢ ((({a ∣ ∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) ∈ V ∧ Ncfin V ∈
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) ∧ ∀w ∈ Spfin ∀z((w ∈ ({a ∣ ∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V}) ∧ Sfin
(z, w))
→ z ∈ ({a ∣ ∃x ∈ Spfin a =
Tfin x} ∪ { Ncfin V}))) → Spfin ⊆
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V})) |
93 | 87, 91, 92 | mp3an12 1267 |
. 2
⊢ (∀w ∈ Spfin
∀z((w ∈ ({a ∣ ∃x ∈ Spfin a =
Tfin x} ∪ { Ncfin V}) ∧
Sfin (z, w)) →
z ∈
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V})) → Spfin ⊆
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V})) |
94 | 58, 93 | syl 15 |
1
⊢ (V ∈ Fin → Spfin ⊆
({a ∣
∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V})) |