Theorem sfintfin 4533

Description: If two numbers obey S_fin, then do their T raisings. Theorem X.1.45 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)

Assertion

Ref	Expression
sfintfin	⊢ ( Sfin (M, N) → Sfin ( Tfin M, Tfin N))

Proof of Theorem sfintfin

Dummy variables a k m n p q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sfin 4447	. . 3 ⊢ ( Sfin (M, N) ↔ (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)))
2		3simpa 952	. . 3 ⊢ ((M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)) → (M ∈ Nn ∧ N ∈ Nn ))
3	1, 2	sylbi 187	. 2 ⊢ ( Sfin (M, N) → (M ∈ Nn ∧ N ∈ Nn ))
4		sfintfinlem1 4532	. . . 4 ⊢ {k ∣ ∀n( Sfin (k, n) → Sfin ( Tfin k, Tfin n))} ∈ V
5		sfineq1 4527	. . . . . 6 ⊢ (k = 0c → ( Sfin (k, n) ↔ Sfin (0c, n)))
6		tfineq 4489	. . . . . . . 8 ⊢ (k = 0c → Tfin k = Tfin 0c)
7		tfin0c 4498	. . . . . . . 8 ⊢ Tfin 0c = 0c
8	6, 7	syl6eq 2401	. . . . . . 7 ⊢ (k = 0c → Tfin k = 0c)
9		sfineq1 4527	. . . . . . 7 ⊢ ( Tfin k = 0c → ( Sfin ( Tfin k, Tfin n) ↔ Sfin (0c, Tfin n)))
10	8, 9	syl 15	. . . . . 6 ⊢ (k = 0c → ( Sfin ( Tfin k, Tfin n) ↔ Sfin (0c, Tfin n)))
11	5, 10	imbi12d 311	. . . . 5 ⊢ (k = 0c → (( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ( Sfin (0c, n) → Sfin (0c, Tfin n))))
12	11	albidv 1625	. . . 4 ⊢ (k = 0c → (∀n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ∀n( Sfin (0c, n) → Sfin (0c, Tfin n))))
13		sfineq1 4527	. . . . . . 7 ⊢ (k = m → ( Sfin (k, n) ↔ Sfin (m, n)))
14		tfineq 4489	. . . . . . . 8 ⊢ (k = m → Tfin k = Tfin m)
15		sfineq1 4527	. . . . . . . 8 ⊢ ( Tfin k = Tfin m → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin m, Tfin n)))
16	14, 15	syl 15	. . . . . . 7 ⊢ (k = m → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin m, Tfin n)))
17	13, 16	imbi12d 311	. . . . . 6 ⊢ (k = m → (( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ( Sfin (m, n) → Sfin ( Tfin m, Tfin n))))
18	17	albidv 1625	. . . . 5 ⊢ (k = m → (∀n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ∀n( Sfin (m, n) → Sfin ( Tfin m, Tfin n))))
19		sfineq2 4528	. . . . . . 7 ⊢ (n = p → ( Sfin (m, n) ↔ Sfin (m, p)))
20		tfineq 4489	. . . . . . . 8 ⊢ (n = p → Tfin n = Tfin p)
21		sfineq2 4528	. . . . . . . 8 ⊢ ( Tfin n = Tfin p → ( Sfin ( Tfin m, Tfin n) ↔ Sfin ( Tfin m, Tfin p)))
22	20, 21	syl 15	. . . . . . 7 ⊢ (n = p → ( Sfin ( Tfin m, Tfin n) ↔ Sfin ( Tfin m, Tfin p)))
23	19, 22	imbi12d 311	. . . . . 6 ⊢ (n = p → (( Sfin (m, n) → Sfin ( Tfin m, Tfin n)) ↔ ( Sfin (m, p) → Sfin ( Tfin m, Tfin p))))
24	23	cbvalv 2002	. . . . 5 ⊢ (∀n( Sfin (m, n) → Sfin ( Tfin m, Tfin n)) ↔ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)))
25	18, 24	syl6bb 252	. . . 4 ⊢ (k = m → (∀n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p))))
26		sfineq1 4527	. . . . . 6 ⊢ (k = (m +c 1c) → ( Sfin (k, n) ↔ Sfin ((m +c 1c), n)))
27		tfineq 4489	. . . . . . 7 ⊢ (k = (m +c 1c) → Tfin k = Tfin (m +c 1c))
28		sfineq1 4527	. . . . . . 7 ⊢ ( Tfin k = Tfin (m +c 1c) → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin (m +c 1c), Tfin n)))
29	27, 28	syl 15	. . . . . 6 ⊢ (k = (m +c 1c) → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin (m +c 1c), Tfin n)))
30	26, 29	imbi12d 311	. . . . 5 ⊢ (k = (m +c 1c) → (( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n))))
31	30	albidv 1625	. . . 4 ⊢ (k = (m +c 1c) → (∀n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ∀n( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n))))
32		sfineq1 4527	. . . . . 6 ⊢ (k = M → ( Sfin (k, n) ↔ Sfin (M, n)))
33		tfineq 4489	. . . . . . 7 ⊢ (k = M → Tfin k = Tfin M)
34		sfineq1 4527	. . . . . . 7 ⊢ ( Tfin k = Tfin M → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin M, Tfin n)))
35	33, 34	syl 15	. . . . . 6 ⊢ (k = M → ( Sfin ( Tfin k, Tfin n) ↔ Sfin ( Tfin M, Tfin n)))
36	32, 35	imbi12d 311	. . . . 5 ⊢ (k = M → (( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ( Sfin (M, n) → Sfin ( Tfin M, Tfin n))))
37	36	albidv 1625	. . . 4 ⊢ (k = M → (∀n( Sfin (k, n) → Sfin ( Tfin k, Tfin n)) ↔ ∀n( Sfin (M, n) → Sfin ( Tfin M, Tfin n))))
38		sfin01 4529	. . . . . . 7 ⊢ Sfin (0c, 1c)
39		sfin112 4530	. . . . . . 7 ⊢ (( Sfin (0c, n) ∧ Sfin (0c, 1c)) → n = 1c)
40	38, 39	mpan2 652	. . . . . 6 ⊢ ( Sfin (0c, n) → n = 1c)
41		tfineq 4489	. . . . . . . . 9 ⊢ (n = 1c → Tfin n = Tfin 1c)
42		tfin1c 4500	. . . . . . . . 9 ⊢ Tfin 1c = 1c
43	41, 42	syl6eq 2401	. . . . . . . 8 ⊢ (n = 1c → Tfin n = 1c)
44		sfineq2 4528	. . . . . . . 8 ⊢ ( Tfin n = 1c → ( Sfin (0c, Tfin n) ↔ Sfin (0c, 1c)))
45	43, 44	syl 15	. . . . . . 7 ⊢ (n = 1c → ( Sfin (0c, Tfin n) ↔ Sfin (0c, 1c)))
46	38, 45	mpbiri 224	. . . . . 6 ⊢ (n = 1c → Sfin (0c, Tfin n))
47	40, 46	syl 15	. . . . 5 ⊢ ( Sfin (0c, n) → Sfin (0c, Tfin n))
48	47	ax-gen 1546	. . . 4 ⊢ ∀n( Sfin (0c, n) → Sfin (0c, Tfin n))
49		df-sfin 4447	. . . . . . . . . 10 ⊢ ( Sfin ((m +c 1c), n) ↔ ((m +c 1c) ∈ Nn ∧ n ∈ Nn ∧ ∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ n)))
50	49	simp3bi 972	. . . . . . . . 9 ⊢ ( Sfin ((m +c 1c), n) → ∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ n))
51	50	3ad2ant3 978	. . . . . . . 8 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) → ∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ n))
52		sfindbl 4531	. . . . . . . . . . . . 13 ⊢ ((m ∈ Nn ∧ ℘1a ∈ (m +c 1c)) → ∃q ∈ Nn ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q))))
53	52	3ad2antl1 1117	. . . . . . . . . . . 12 ⊢ (((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) ∧ ℘1a ∈ (m +c 1c)) → ∃q ∈ Nn ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q))))
54		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (p = q → ( Sfin (m, p) ↔ Sfin (m, q)))
55		tfineq 4489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (p = q → Tfin p = Tfin q)
56		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ( Tfin p = Tfin q → ( Sfin ( Tfin m, Tfin p) ↔ Sfin ( Tfin m, Tfin q)))
57	55, 56	syl 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (p = q → ( Sfin ( Tfin m, Tfin p) ↔ Sfin ( Tfin m, Tfin q)))
58	54, 57	imbi12d 311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (p = q → (( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ↔ ( Sfin (m, q) → Sfin ( Tfin m, Tfin q))))
59	58	spv 1998	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → ( Sfin (m, q) → Sfin ( Tfin m, Tfin q)))
60		simprrl 740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q))))) → Sfin (m, q))
61	60	adantl 452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) → Sfin (m, q))
62		simplrl 736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → Sfin ((m +c 1c), n))
63		simprrr 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q))))) → Sfin ((m +c 1c), (q +c q)))
64	63	ad2antlr 707	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → Sfin ((m +c 1c), (q +c q)))
65		sfin112 4530	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (( Sfin ((m +c 1c), n) ∧ Sfin ((m +c 1c), (q +c q))) → n = (q +c q))
66	62, 64, 65	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → n = (q +c q))
67		df-sfin 4447	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ( Sfin ((m +c 1c), (q +c q)) ↔ ((m +c 1c) ∈ Nn ∧ (q +c q) ∈ Nn ∧ ∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ (q +c q))))
68	67	simp3bi 972	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ( Sfin ((m +c 1c), (q +c q)) → ∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ (q +c q)))
69	64, 68	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → ∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ (q +c q)))
70		simp2 956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → Sfin ( Tfin m, Tfin q))
71		df-sfin 4447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ( Sfin ( Tfin m, Tfin q) ↔ ( Tfin m ∈ Nn ∧ Tfin q ∈ Nn ∧ ∃a(℘1a ∈ Tfin m ∧ ℘a ∈ Tfin q)))
72	71	simp1bi 970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ( Sfin ( Tfin m, Tfin q) → Tfin m ∈ Nn )
73	70, 72	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → Tfin m ∈ Nn )
74		simp1l 979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → m ∈ Nn )
75		peano2 4404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (m ∈ Nn → (m +c 1c) ∈ Nn )
76	74, 75	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → (m +c 1c) ∈ Nn )
77		simp3 957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → ℘1a ∈ (m +c 1c))
78		tfinpw1 4495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((m +c 1c) ∈ Nn ∧ ℘1a ∈ (m +c 1c)) → ℘1℘1a ∈ Tfin (m +c 1c))
79	76, 77, 78	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → ℘1℘1a ∈ Tfin (m +c 1c))
80		ne0i 3557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (℘1a ∈ (m +c 1c) → (m +c 1c) ≠ ∅)
81	80	3ad2ant3 978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → (m +c 1c) ≠ ∅)
82		tfinsuc 4499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((m ∈ Nn ∧ (m +c 1c) ≠ ∅) → Tfin (m +c 1c) = ( Tfin m +c 1c))
83	74, 81, 82	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → Tfin (m +c 1c) = ( Tfin m +c 1c))
84	79, 83	eleqtrd 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → ℘1℘1a ∈ ( Tfin m +c 1c))
85		sfindbl 4531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (( Tfin m ∈ Nn ∧ ℘1℘1a ∈ ( Tfin m +c 1c)) → ∃k ∈ Nn ( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k))))
86	73, 84, 85	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → ∃k ∈ Nn ( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k))))
87		simp2 956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k)))) → Sfin ( Tfin m, Tfin q))
88		simp3l 983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k)))) → Sfin ( Tfin m, k))
89		sfin112 4530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (( Sfin ( Tfin m, Tfin q) ∧ Sfin ( Tfin m, k)) → Tfin q = k)
90	87, 88, 89	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k)))) → Tfin q = k)
91		addceq12 4386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (( Tfin q = k ∧ Tfin q = k) → ( Tfin q +c Tfin q) = (k +c k))
92	91	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ( Tfin q = k → ( Tfin q +c Tfin q) = (k +c k))
93		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (( Tfin q +c Tfin q) = (k +c k) → ( Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)) ↔ Sfin (( Tfin m +c 1c), (k +c k))))
94	92, 93	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ( Tfin q = k → ( Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)) ↔ Sfin (( Tfin m +c 1c), (k +c k))))
95	94	biimprcd 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ( Sfin (( Tfin m +c 1c), (k +c k)) → ( Tfin q = k → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
96	95	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k))) → ( Tfin q = k → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
97	96	3ad2ant3 978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k)))) → ( Tfin q = k → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
98	90, 97	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k)))) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)))
99	98	3expia 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → (( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k))) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
100	99	rexlimdvw 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → (∃k ∈ Nn ( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k))) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
101	100	3adant3 975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → (∃k ∈ Nn ( Sfin ( Tfin m, k) ∧ Sfin (( Tfin m +c 1c), (k +c k))) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
102	86, 101	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q) ∧ ℘1a ∈ (m +c 1c)) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)))
103	102	3expia 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → (℘1a ∈ (m +c 1c) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
104	103	adantrd 454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → ((℘1a ∈ (m +c 1c) ∧ ℘a ∈ (q +c q)) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
105	104	exlimdv 1636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → (∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ (q +c q)) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
106	69, 105	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q)))
107		simpll 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → m ∈ Nn )
108	80	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((℘1a ∈ (m +c 1c) ∧ ℘a ∈ (q +c q)) → (m +c 1c) ≠ ∅)
109	108	exlimiv 1634	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ (q +c q)) → (m +c 1c) ≠ ∅)
110	64, 68, 109	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → (m +c 1c) ≠ ∅)
111	107, 110, 82	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → Tfin (m +c 1c) = ( Tfin m +c 1c))
112		simprrl 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) → q ∈ Nn )
113	112	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → q ∈ Nn )
114		ne0i 3557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (℘a ∈ (q +c q) → (q +c q) ≠ ∅)
115	114	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((℘1a ∈ (m +c 1c) ∧ ℘a ∈ (q +c q)) → (q +c q) ≠ ∅)
116	115	exlimiv 1634	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ (q +c q)) → (q +c q) ≠ ∅)
117	64, 68, 116	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → (q +c q) ≠ ∅)
118		tfindi 4497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((q ∈ Nn ∧ q ∈ Nn ∧ (q +c q) ≠ ∅) → Tfin (q +c q) = ( Tfin q +c Tfin q))
119	113, 113, 117, 118	syl3anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → Tfin (q +c q) = ( Tfin q +c Tfin q))
120		sfineq1 4527	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ( Tfin (m +c 1c) = ( Tfin m +c 1c) → ( Sfin ( Tfin (m +c 1c), Tfin (q +c q)) ↔ Sfin (( Tfin m +c 1c), Tfin (q +c q))))
121		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ( Tfin (q +c q) = ( Tfin q +c Tfin q) → ( Sfin (( Tfin m +c 1c), Tfin (q +c q)) ↔ Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
122	120, 121	sylan9bb 680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (( Tfin (m +c 1c) = ( Tfin m +c 1c) ∧ Tfin (q +c q) = ( Tfin q +c Tfin q)) → ( Sfin ( Tfin (m +c 1c), Tfin (q +c q)) ↔ Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
123	111, 119, 122	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → ( Sfin ( Tfin (m +c 1c), Tfin (q +c q)) ↔ Sfin (( Tfin m +c 1c), ( Tfin q +c Tfin q))))
124	106, 123	mpbird 223	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → Sfin ( Tfin (m +c 1c), Tfin (q +c q)))
125		tfineq 4489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (n = (q +c q) → Tfin n = Tfin (q +c q))
126		sfineq2 4528	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ( Tfin n = Tfin (q +c q) → ( Sfin ( Tfin (m +c 1c), Tfin n) ↔ Sfin ( Tfin (m +c 1c), Tfin (q +c q))))
127	125, 126	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (n = (q +c q) → ( Sfin ( Tfin (m +c 1c), Tfin n) ↔ Sfin ( Tfin (m +c 1c), Tfin (q +c q))))
128	127	biimprcd 216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ( Sfin ( Tfin (m +c 1c), Tfin (q +c q)) → (n = (q +c q) → Sfin ( Tfin (m +c 1c), Tfin n)))
129	124, 128	syl 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → (n = (q +c q) → Sfin ( Tfin (m +c 1c), Tfin n)))
130	66, 129	mpd 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) ∧ Sfin ( Tfin m, Tfin q)) → Sfin ( Tfin (m +c 1c), Tfin n))
131	130	ex 423	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) → ( Sfin ( Tfin m, Tfin q) → Sfin ( Tfin (m +c 1c), Tfin n)))
132	61, 131	embantd 50	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) → (( Sfin (m, q) → Sfin ( Tfin m, Tfin q)) → Sfin ( Tfin (m +c 1c), Tfin n)))
133	59, 132	syl5 28	. . . . . . . . . . . . . . . . . . 19 ⊢ ((m ∈ Nn ∧ ( Sfin ((m +c 1c), n) ∧ (q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))))) → (∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → Sfin ( Tfin (m +c 1c), Tfin n)))
134	133	exp32 588	. . . . . . . . . . . . . . . . . 18 ⊢ (m ∈ Nn → ( Sfin ((m +c 1c), n) → ((q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))) → (∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → Sfin ( Tfin (m +c 1c), Tfin n)))))
135	134	com34 77	. . . . . . . . . . . . . . . . 17 ⊢ (m ∈ Nn → ( Sfin ((m +c 1c), n) → (∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → ((q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))) → Sfin ( Tfin (m +c 1c), Tfin n)))))
136	135	com23 72	. . . . . . . . . . . . . . . 16 ⊢ (m ∈ Nn → (∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → ( Sfin ((m +c 1c), n) → ((q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))) → Sfin ( Tfin (m +c 1c), Tfin n)))))
137	136	3imp 1145	. . . . . . . . . . . . . . 15 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) → ((q ∈ Nn ∧ ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q)))) → Sfin ( Tfin (m +c 1c), Tfin n)))
138	137	exp3a 425	. . . . . . . . . . . . . 14 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) → (q ∈ Nn → (( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q))) → Sfin ( Tfin (m +c 1c), Tfin n))))
139	138	rexlimdv 2738	. . . . . . . . . . . . 13 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) → (∃q ∈ Nn ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q))) → Sfin ( Tfin (m +c 1c), Tfin n)))
140	139	adantr 451	. . . . . . . . . . . 12 ⊢ (((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) ∧ ℘1a ∈ (m +c 1c)) → (∃q ∈ Nn ( Sfin (m, q) ∧ Sfin ((m +c 1c), (q +c q))) → Sfin ( Tfin (m +c 1c), Tfin n)))
141	53, 140	mpd 14	. . . . . . . . . . 11 ⊢ (((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) ∧ ℘1a ∈ (m +c 1c)) → Sfin ( Tfin (m +c 1c), Tfin n))
142	141	ex 423	. . . . . . . . . 10 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) → (℘1a ∈ (m +c 1c) → Sfin ( Tfin (m +c 1c), Tfin n)))
143	142	adantrd 454	. . . . . . . . 9 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) → ((℘1a ∈ (m +c 1c) ∧ ℘a ∈ n) → Sfin ( Tfin (m +c 1c), Tfin n)))
144	143	exlimdv 1636	. . . . . . . 8 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) → (∃a(℘1a ∈ (m +c 1c) ∧ ℘a ∈ n) → Sfin ( Tfin (m +c 1c), Tfin n)))
145	51, 144	mpd 14	. . . . . . 7 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) ∧ Sfin ((m +c 1c), n)) → Sfin ( Tfin (m +c 1c), Tfin n))
146	145	3expia 1153	. . . . . 6 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p))) → ( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n)))
147	146	alrimiv 1631	. . . . 5 ⊢ ((m ∈ Nn ∧ ∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p))) → ∀n( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n)))
148	147	ex 423	. . . 4 ⊢ (m ∈ Nn → (∀p( Sfin (m, p) → Sfin ( Tfin m, Tfin p)) → ∀n( Sfin ((m +c 1c), n) → Sfin ( Tfin (m +c 1c), Tfin n))))
149	4, 12, 25, 31, 37, 48, 148	finds 4412	. . 3 ⊢ (M ∈ Nn → ∀n( Sfin (M, n) → Sfin ( Tfin M, Tfin n)))
150		sfineq2 4528	. . . . 5 ⊢ (n = N → ( Sfin (M, n) ↔ Sfin (M, N)))
151		tfineq 4489	. . . . . 6 ⊢ (n = N → Tfin n = Tfin N)
152		sfineq2 4528	. . . . . 6 ⊢ ( Tfin n = Tfin N → ( Sfin ( Tfin M, Tfin n) ↔ Sfin ( Tfin M, Tfin N)))
153	151, 152	syl 15	. . . . 5 ⊢ (n = N → ( Sfin ( Tfin M, Tfin n) ↔ Sfin ( Tfin M, Tfin N)))
154	150, 153	imbi12d 311	. . . 4 ⊢ (n = N → (( Sfin (M, n) → Sfin ( Tfin M, Tfin n)) ↔ ( Sfin (M, N) → Sfin ( Tfin M, Tfin N))))
155	154	spcgv 2940	. . 3 ⊢ (N ∈ Nn → (∀n( Sfin (M, n) → Sfin ( Tfin M, Tfin n)) → ( Sfin (M, N) → Sfin ( Tfin M, Tfin N))))
156	149, 155	mpan9 455	. 2 ⊢ ((M ∈ Nn ∧ N ∈ Nn ) → ( Sfin (M, N) → Sfin ( Tfin M, Tfin N)))
157	3, 156	mpcom 32	1 ⊢ ( Sfin (M, N) → Sfin ( Tfin M, Tfin N))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710   ≠ wne 2517  ∃wrex 2616  ∅c0 3551  ℘cpw 3723  1_cc1c 4135  ℘₁cpw1 4136   Nn cnnc 4374  0_cc0c 4375   +_c cplc 4376   T_fin ctfin 4436   S_fin wsfin 4439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-tfin 4444  df-sfin 4447

This theorem is referenced by:  t1csfin1c  4546  vfinspsslem1  4551  vfinspclt  4553