Step |
Hyp |
Ref |
Expression |
1 |
|
raleq |
⊢ ( 𝑥 = ∅ → ( ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∀ 𝑛 ∈ ∅ 𝜑 ) ) |
2 |
1
|
rexralbidv |
⊢ ( 𝑥 = ∅ → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ∅ 𝜑 ) ) |
3 |
|
raleq |
⊢ ( 𝑥 = ∅ → ( ∀ 𝑛 ∈ 𝑥 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∀ 𝑛 ∈ ∅ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
4 |
2 3
|
bibi12d |
⊢ ( 𝑥 = ∅ → ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∀ 𝑛 ∈ 𝑥 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ∅ 𝜑 ↔ ∀ 𝑛 ∈ ∅ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) ) |
5 |
|
raleq |
⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∀ 𝑛 ∈ 𝑦 𝜑 ) ) |
6 |
5
|
rexralbidv |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ) ) |
7 |
|
raleq |
⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑛 ∈ 𝑥 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∀ 𝑛 ∈ 𝑦 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
8 |
6 7
|
bibi12d |
⊢ ( 𝑥 = 𝑦 → ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∀ 𝑛 ∈ 𝑥 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ↔ ∀ 𝑛 ∈ 𝑦 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) ) |
9 |
|
raleq |
⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝜑 ) ) |
10 |
9
|
rexralbidv |
⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝜑 ) ) |
11 |
|
raleq |
⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑛 ∈ 𝑥 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
12 |
10 11
|
bibi12d |
⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∀ 𝑛 ∈ 𝑥 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝜑 ↔ ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) ) |
13 |
|
raleq |
⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∀ 𝑛 ∈ 𝐴 𝜑 ) ) |
14 |
13
|
rexralbidv |
⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝐴 𝜑 ) ) |
15 |
|
raleq |
⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑛 ∈ 𝑥 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∀ 𝑛 ∈ 𝐴 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
16 |
14 15
|
bibi12d |
⊢ ( 𝑥 = 𝐴 → ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑥 𝜑 ↔ ∀ 𝑛 ∈ 𝑥 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝐴 𝜑 ↔ ∀ 𝑛 ∈ 𝐴 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) ) |
17 |
|
0z |
⊢ 0 ∈ ℤ |
18 |
17
|
ne0ii |
⊢ ℤ ≠ ∅ |
19 |
|
ral0 |
⊢ ∀ 𝑛 ∈ ∅ 𝜑 |
20 |
19
|
rgen2w |
⊢ ∀ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ∅ 𝜑 |
21 |
|
r19.2z |
⊢ ( ( ℤ ≠ ∅ ∧ ∀ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ∅ 𝜑 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ∅ 𝜑 ) |
22 |
18 20 21
|
mp2an |
⊢ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ∅ 𝜑 |
23 |
|
ral0 |
⊢ ∀ 𝑛 ∈ ∅ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 |
24 |
22 23
|
2th |
⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ∅ 𝜑 ↔ ∀ 𝑛 ∈ ∅ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) |
25 |
|
anbi1 |
⊢ ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ↔ ∀ 𝑛 ∈ 𝑦 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ∧ ∀ 𝑛 ∈ { 𝑧 } ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ↔ ( ∀ 𝑛 ∈ 𝑦 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∀ 𝑛 ∈ { 𝑧 } ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) ) |
26 |
|
rexanuz |
⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ∀ 𝑛 ∈ 𝑦 𝜑 ∧ ∀ 𝑛 ∈ { 𝑧 } 𝜑 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ { 𝑧 } 𝜑 ) ) |
27 |
|
ralunb |
⊢ ( ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝜑 ↔ ( ∀ 𝑛 ∈ 𝑦 𝜑 ∧ ∀ 𝑛 ∈ { 𝑧 } 𝜑 ) ) |
28 |
27
|
ralbii |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝜑 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ∀ 𝑛 ∈ 𝑦 𝜑 ∧ ∀ 𝑛 ∈ { 𝑧 } 𝜑 ) ) |
29 |
28
|
rexbii |
⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ∀ 𝑛 ∈ 𝑦 𝜑 ∧ ∀ 𝑛 ∈ { 𝑧 } 𝜑 ) ) |
30 |
|
ralsnsg |
⊢ ( 𝑧 ∈ V → ( ∀ 𝑛 ∈ { 𝑧 } ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ [ 𝑧 / 𝑛 ] ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
31 |
|
sbcrex |
⊢ ( [ 𝑧 / 𝑛 ] ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℤ [ 𝑧 / 𝑛 ] ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) |
32 |
|
ralcom |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ { 𝑧 } 𝜑 ↔ ∀ 𝑛 ∈ { 𝑧 } ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) |
33 |
|
ralsnsg |
⊢ ( 𝑧 ∈ V → ( ∀ 𝑛 ∈ { 𝑧 } ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ [ 𝑧 / 𝑛 ] ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
34 |
32 33
|
syl5bb |
⊢ ( 𝑧 ∈ V → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ { 𝑧 } 𝜑 ↔ [ 𝑧 / 𝑛 ] ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
35 |
34
|
rexbidv |
⊢ ( 𝑧 ∈ V → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ { 𝑧 } 𝜑 ↔ ∃ 𝑗 ∈ ℤ [ 𝑧 / 𝑛 ] ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
36 |
31 35
|
bitr4id |
⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑛 ] ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ { 𝑧 } 𝜑 ) ) |
37 |
30 36
|
bitrd |
⊢ ( 𝑧 ∈ V → ( ∀ 𝑛 ∈ { 𝑧 } ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ { 𝑧 } 𝜑 ) ) |
38 |
37
|
elv |
⊢ ( ∀ 𝑛 ∈ { 𝑧 } ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ { 𝑧 } 𝜑 ) |
39 |
38
|
anbi2i |
⊢ ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ∧ ∀ 𝑛 ∈ { 𝑧 } ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ { 𝑧 } 𝜑 ) ) |
40 |
26 29 39
|
3bitr4i |
⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝜑 ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ∧ ∀ 𝑛 ∈ { 𝑧 } ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
41 |
|
ralunb |
⊢ ( ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ( ∀ 𝑛 ∈ 𝑦 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∀ 𝑛 ∈ { 𝑧 } ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
42 |
25 40 41
|
3bitr4g |
⊢ ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ↔ ∀ 𝑛 ∈ 𝑦 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝜑 ↔ ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |
43 |
42
|
a1i |
⊢ ( 𝑦 ∈ Fin → ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝑦 𝜑 ↔ ∀ 𝑛 ∈ 𝑦 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝜑 ↔ ∀ 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) ) |
44 |
4 8 12 16 24 43
|
findcard2 |
⊢ ( 𝐴 ∈ Fin → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑛 ∈ 𝐴 𝜑 ↔ ∀ 𝑛 ∈ 𝐴 ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) |