Theorem sadcf

Description: The carry sequence is a sequence of elements of 2o encoding a "sequence of wffs". (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Hypotheses	sadval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	sadval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	sadval.c	⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
Assertion	sadcf	⊢ ( 𝜑 → 𝐶 : ℕ0 ⟶ 2o )

Proof

Step	Hyp	Ref	Expression
1		sadval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		sadval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		sadval.c	⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4		0nn0	⊢ 0 ∈ ℕ0
5		iftrue	⊢ ( 𝑛 = 0 → if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) = ∅ )
6		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) )
7		0ex	⊢ ∅ ∈ V
8	5 6 7	fvmpt	⊢ ( 0 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) = ∅ )
9	4 8	ax-mp	⊢ ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) = ∅
10	7	prid1	⊢ ∅ ∈ { ∅ , 1o }
11		df2o3	⊢ 2o = { ∅ , 1o }
12	10 11	eleqtrri	⊢ ∅ ∈ 2o
13	9 12	eqeltri	⊢ ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) ∈ 2o
14	13	a1i	⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) ∈ 2o )
15		df-ov	⊢ ( 𝑥 ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) 𝑦 ) = ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
16		1oelpr	⊢ 1o ∈ { ∅ , 1o }
17	16 11	eleqtrri	⊢ 1o ∈ 2o
18	17 12	ifcli	⊢ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ∈ 2o
19	18	rgen2w	⊢ ∀ 𝑐 ∈ 2o ∀ 𝑚 ∈ ℕ0 if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ∈ 2o
20		eqid	⊢ ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) = ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) )
21	20	fmpo	⊢ ( ∀ 𝑐 ∈ 2o ∀ 𝑚 ∈ ℕ0 if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ∈ 2o ↔ ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) : ( 2o × ℕ0 ) ⟶ 2o )
22	19 21	mpbi	⊢ ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) : ( 2o × ℕ0 ) ⟶ 2o
23	22 12	f0cli	⊢ ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 2o
24	15 23	eqeltri	⊢ ( 𝑥 ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) 𝑦 ) ∈ 2o
25	24	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 2o ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) 𝑦 ) ∈ 2o )
26		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
27		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
28		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 𝑥 ) ∈ V )
29	14 25 26 27 28	seqf2	⊢ ( 𝜑 → seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) : ℕ0 ⟶ 2o )
30	3	feq1i	⊢ ( 𝐶 : ℕ0 ⟶ 2o ↔ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) : ℕ0 ⟶ 2o )
31	29 30	sylibr	⊢ ( 𝜑 → 𝐶 : ℕ0 ⟶ 2o )