Theorem axdc4uz

Description: A version of axdc4 that works on an upper set of integers instead of _om . (Contributed by Mario Carneiro, 8-Jan-2014)

	Ref	Expression
Hypotheses	axdc4uz.1	⊢ 𝑀 ∈ ℤ
	axdc4uz.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	axdc4uz	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axdc4uz.1	⊢ 𝑀 ∈ ℤ
2		axdc4uz.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		eleq2	⊢ ( 𝑓 = 𝐴 → ( 𝐶 ∈ 𝑓 ↔ 𝐶 ∈ 𝐴 ) )
4		xpeq2	⊢ ( 𝑓 = 𝐴 → ( 𝑍 × 𝑓 ) = ( 𝑍 × 𝐴 ) )
5		pweq	⊢ ( 𝑓 = 𝐴 → 𝒫 𝑓 = 𝒫 𝐴 )
6	5	difeq1d	⊢ ( 𝑓 = 𝐴 → ( 𝒫 𝑓 ∖ { ∅ } ) = ( 𝒫 𝐴 ∖ { ∅ } ) )
7	4 6	feq23d	⊢ ( 𝑓 = 𝐴 → ( 𝐹 : ( 𝑍 × 𝑓 ) ⟶ ( 𝒫 𝑓 ∖ { ∅ } ) ↔ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) )
8	3 7	anbi12d	⊢ ( 𝑓 = 𝐴 → ( ( 𝐶 ∈ 𝑓 ∧ 𝐹 : ( 𝑍 × 𝑓 ) ⟶ ( 𝒫 𝑓 ∖ { ∅ } ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) ) )
9		feq3	⊢ ( 𝑓 = 𝐴 → ( 𝑔 : 𝑍 ⟶ 𝑓 ↔ 𝑔 : 𝑍 ⟶ 𝐴 ) )
10	9	3anbi1d	⊢ ( 𝑓 = 𝐴 → ( ( 𝑔 : 𝑍 ⟶ 𝑓 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ↔ ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) )
11	10	exbidv	⊢ ( 𝑓 = 𝐴 → ( ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝑓 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) )
12	8 11	imbi12d	⊢ ( 𝑓 = 𝐴 → ( ( ( 𝐶 ∈ 𝑓 ∧ 𝐹 : ( 𝑍 × 𝑓 ) ⟶ ( 𝒫 𝑓 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝑓 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) ) )
13		vex	⊢ 𝑓 ∈ V
14		eqid	⊢ ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω )
15		eqid	⊢ ( 𝑛 ∈ ω , 𝑥 ∈ 𝑓 ↦ ( ( ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω ) ‘ 𝑛 ) 𝐹 𝑥 ) ) = ( 𝑛 ∈ ω , 𝑥 ∈ 𝑓 ↦ ( ( ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω ) ‘ 𝑛 ) 𝐹 𝑥 ) )
16	1 2 13 14 15	axdc4uzlem	⊢ ( ( 𝐶 ∈ 𝑓 ∧ 𝐹 : ( 𝑍 × 𝑓 ) ⟶ ( 𝒫 𝑓 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝑓 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )
17	12 16	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) )
18	17	3impib	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )