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