Metamath Proof Explorer


Theorem rexfiuz

Description: Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Assertion rexfiuz ( 𝐴 ∈ Fin → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑛𝐴 𝜑 ↔ ∀ 𝑛𝐴𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) 𝜑 ) )

Proof

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 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑛𝐴 𝜑 ↔ ∀ 𝑛𝐴𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) 𝜑 ) )