findcard4 - Mathbox for Thomas van Maaren

	Mathbox for Thomas van Maaren		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > findcard4		Structured version Visualization version GIF version

Theorem findcard4 38422

Description: Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any set with less elements. The result is then proven to be true for all finite sets. (Contributed by Thomas van Maaren, 14-Aug-2026.)

**Hypotheses**
Ref	Expression
findcard4.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
findcard4.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
findcard4.3	⊢ (𝑦 ∈ Fin → (∀𝑥((♯‘𝑥) < (♯‘𝑦) → 𝜑) → 𝜒))

**Assertion**
Ref	Expression
findcard4	⊢ (𝐴 ∈ Fin → 𝜏)

Distinct variable groups: 𝜒,𝑥 𝜏,𝑥 𝑥,𝑦 𝑥,𝐴 𝜑,𝑦 Allowed substitution hints: 𝜑(𝑥) 𝜒(𝑦) 𝜏(𝑦) 𝐴(𝑦)

Proof of Theorem findcard4 Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ficardom 9963	. . . 4 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
2		nnfi 9159	. . . 4 ⊢ ((card‘𝐴) ∈ ω → (card‘𝐴) ∈ Fin)
3	1, 2	syl 18	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ Fin)
4		fveq2 6885	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (card‘𝑥) = (card‘𝑦))
5	4	adantl 487	. . . . . . 7 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (card‘𝑥) = (card‘𝑦))
6		simpl 488	. . . . . . 7 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → 𝑤 = 𝑧)
7	5, 6	eqeq12d 2781	. . . . . 6 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → ((card‘𝑥) = 𝑤 ↔ (card‘𝑦) = 𝑧))
8		findcard4.1	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
9	8	adantl 487	. . . . . 6 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (𝜑 ↔ 𝜒))
10	7, 9	imbi12d 347	. . . . 5 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (((card‘𝑥) = 𝑤 → 𝜑) ↔ ((card‘𝑦) = 𝑧 → 𝜒)))
11	10	cbvaldvaw 2071	. . . 4 ⊢ (𝑤 = 𝑧 → (∀𝑥((card‘𝑥) = 𝑤 → 𝜑) ↔ ∀𝑦((card‘𝑦) = 𝑧 → 𝜒)))
12		eqeq2 2777	. . . . . 6 ⊢ (𝑤 = (card‘𝐴) → ((card‘𝑥) = 𝑤 ↔ (card‘𝑥) = (card‘𝐴)))
13	12	imbi1d 344	. . . . 5 ⊢ (𝑤 = (card‘𝐴) → (((card‘𝑥) = 𝑤 → 𝜑) ↔ ((card‘𝑥) = (card‘𝐴) → 𝜑)))
14	13	albidv 1953	. . . 4 ⊢ (𝑤 = (card‘𝐴) → (∀𝑥((card‘𝑥) = 𝑤 → 𝜑) ↔ ∀𝑥((card‘𝑥) = (card‘𝐴) → 𝜑)))
15		eleq1 2853	. . . . . . . . . 10 ⊢ ((card‘𝑦) = 𝑧 → ((card‘𝑦) ∈ Fin ↔ 𝑧 ∈ Fin))
16		vex 3461	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
17	16	cardid 10546	. . . . . . . . . . 11 ⊢ (card‘𝑦) ≈ 𝑦
18		enfi 9178	. . . . . . . . . . 11 ⊢ ((card‘𝑦) ≈ 𝑦 → ((card‘𝑦) ∈ Fin ↔ 𝑦 ∈ Fin))
19	17, 18	ax-mp 5	. . . . . . . . . 10 ⊢ ((card‘𝑦) ∈ Fin ↔ 𝑦 ∈ Fin)
20	15, 19	bitr3di 289	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (𝑧 ∈ Fin ↔ 𝑦 ∈ Fin))
21	20	biimpd 232	. . . . . . . 8 ⊢ ((card‘𝑦) = 𝑧 → (𝑧 ∈ Fin → 𝑦 ∈ Fin))
22		psseq2 4046	. . . . . . . . . . . . 13 ⊢ ((card‘𝑦) = 𝑧 → (𝑤 ⊊ (card‘𝑦) ↔ 𝑤 ⊊ 𝑧))
23	22	bicomd 226	. . . . . . . . . . . 12 ⊢ ((card‘𝑦) = 𝑧 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ (card‘𝑦)))
24	23	imbi1d 344	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → ((𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) ↔ (𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑))))
25		sp 2222	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑤 ⊊ (card‘𝑦) → 𝑤 ⊊ (card‘𝑦))
26	25	imim1i 64	. . . . . . . . . . . 12 ⊢ ((𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → (∀𝑥 𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)))
27		axi5r 2729	. . . . . . . . . . . 12 ⊢ ((∀𝑥 𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥(∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)))
28		ax-5 1943	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ⊊ (card‘𝑦) → ∀𝑥 𝑤 ⊊ (card‘𝑦))
29	28	imim1i 64	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)) → (𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)))
30		eqcom 2772	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (card‘𝑥) ↔ (card‘𝑥) = 𝑤)
31		pm2.04 91	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)) → ((card‘𝑥) = 𝑤 → (𝑤 ⊊ (card‘𝑦) → 𝜑)))
32	30, 31	biimtrid 245	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)) → (𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)))
33	29, 32	syl 18	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)) → (𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)))
34	33	alimi 1844	. . . . . . . . . . . 12 ⊢ (∀𝑥(∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)))
35	26, 27, 34	3syl 19	. . . . . . . . . . 11 ⊢ ((𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)))
36	24, 35	biimtrdi 256	. . . . . . . . . 10 ⊢ ((card‘𝑦) = 𝑧 → ((𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑))))
37	36	alimdv 1949	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑))))
38		ax-11 2195	. . . . . . . . . 10 ⊢ (∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)))
39	38	a1i 11	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑))))
40		nfvd 1948	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → Ⅎ𝑤((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))
41		psseq1 4045	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) ↔ (card‘𝑥) ⊊ (card‘𝑦)))
42	41	imbi1d 344	. . . . . . . . . . . . 13 ⊢ (𝑤 = (card‘𝑥) → ((𝑤 ⊊ (card‘𝑦) → 𝜑) ↔ ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
43	42	a1i 11	. . . . . . . . . . . 12 ⊢ ((card‘𝑦) = 𝑧 → (𝑤 = (card‘𝑥) → ((𝑤 ⊊ (card‘𝑦) → 𝜑) ↔ ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))))
44	43	alrimiv 1960	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → ∀𝑤(𝑤 = (card‘𝑥) → ((𝑤 ⊊ (card‘𝑦) → 𝜑) ↔ ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))))
45		fvexd 6900	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → (card‘𝑥) ∈ V)
46		ceqsalt 3490	. . . . . . . . . . . 12 ⊢ ((Ⅎ𝑤((card‘𝑥) ⊊ (card‘𝑦) → 𝜑) ∧ ∀𝑤(𝑤 = (card‘𝑥) → ((𝑤 ⊊ (card‘𝑦) → 𝜑) ↔ ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))) ∧ (card‘𝑥) ∈ V) → (∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) ↔ ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
47	46	biimpd 232	. . . . . . . . . . 11 ⊢ ((Ⅎ𝑤((card‘𝑥) ⊊ (card‘𝑦) → 𝜑) ∧ ∀𝑤(𝑤 = (card‘𝑥) → ((𝑤 ⊊ (card‘𝑦) → 𝜑) ↔ ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))) ∧ (card‘𝑥) ∈ V) → (∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
48	40, 44, 45, 47	syl3anc 1398	. . . . . . . . . 10 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
49	48	alimdv 1949	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
50	37, 39, 49	3syld 61	. . . . . . . 8 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
51		hashxnn0 14393	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ V → (♯‘𝑥) ∈ ℕ₀^*)
52	51	elv 3462	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘𝑥) ∈ ℕ₀^*
53		hashcl 14410	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
54		hashxrcl 14411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ V → (♯‘𝑥) ∈ ℝ^*)
55	54	elv 3462	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘𝑥) ∈ ℝ^*
56		hashxrcl 14411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ V → (♯‘𝑦) ∈ ℝ^*)
57	56	elv 3462	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘𝑦) ∈ ℝ^*
58		xrltle 13190	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑥) ∈ ℝ^* ∧ (♯‘𝑦) ∈ ℝ^*) → ((♯‘𝑥) < (♯‘𝑦) → (♯‘𝑥) ≤ (♯‘𝑦)))
59	55, 57, 58	mp2an 705	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑥) < (♯‘𝑦) → (♯‘𝑥) ≤ (♯‘𝑦))
60		xnn0lenn0nn0 13287	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑥) ∈ ℕ₀^* ∧ (♯‘𝑦) ∈ ℕ₀ ∧ (♯‘𝑥) ≤ (♯‘𝑦)) → (♯‘𝑥) ∈ ℕ₀)
61	52, 53, 59, 60	mp3an3an 1496	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → (♯‘𝑥) ∈ ℕ₀)
62		hashclb 14412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ V → (𝑥 ∈ Fin ↔ (♯‘𝑥) ∈ ℕ₀))
63	62	elv 3462	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Fin ↔ (♯‘𝑥) ∈ ℕ₀)
64	61, 63	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → 𝑥 ∈ Fin)
65		hashsdom 14435	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → ((♯‘𝑥) < (♯‘𝑦) ↔ 𝑥 ≺ 𝑦))
66		cardsdom 10554	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ((card‘𝑥) ∈ (card‘𝑦) ↔ 𝑥 ≺ 𝑦))
67	66	el2v 3464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((card‘𝑥) ∈ (card‘𝑦) ↔ 𝑥 ≺ 𝑦)
68	65, 67	bitr4di 292	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → ((♯‘𝑥) < (♯‘𝑦) ↔ (card‘𝑥) ∈ (card‘𝑦)))
69	68	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → ((♯‘𝑥) < (♯‘𝑦) → (card‘𝑥) ∈ (card‘𝑦)))
70	69	expimpd 459	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Fin → ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → (card‘𝑥) ∈ (card‘𝑦)))
71	64, 70	mpcom 39	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → (card‘𝑥) ∈ (card‘𝑦))
72	71	ex 418	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → ((♯‘𝑥) < (♯‘𝑦) → (card‘𝑥) ∈ (card‘𝑦)))
73		cardon 9946	. . . . . . . . . . . . . . . 16 ⊢ (card‘𝑥) ∈ On
74	73	onordi 6478	. . . . . . . . . . . . . . 15 ⊢ Ord (card‘𝑥)
75		cardon 9946	. . . . . . . . . . . . . . . 16 ⊢ (card‘𝑦) ∈ On
76	75	onordi 6478	. . . . . . . . . . . . . . 15 ⊢ Ord (card‘𝑦)
77		ordelpss 6392	. . . . . . . . . . . . . . 15 ⊢ ((Ord (card‘𝑥) ∧ Ord (card‘𝑦)) → ((card‘𝑥) ∈ (card‘𝑦) ↔ (card‘𝑥) ⊊ (card‘𝑦)))
78	74, 76, 77	mp2an 705	. . . . . . . . . . . . . 14 ⊢ ((card‘𝑥) ∈ (card‘𝑦) ↔ (card‘𝑥) ⊊ (card‘𝑦))
79	72, 78	imbitrdi 254	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → ((♯‘𝑥) < (♯‘𝑦) → (card‘𝑥) ⊊ (card‘𝑦)))
80	79	imim1d 83	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ Fin → (((card‘𝑥) ⊊ (card‘𝑦) → 𝜑) → ((♯‘𝑥) < (♯‘𝑦) → 𝜑)))
81	80	alimdv 1949	. . . . . . . . . . 11 ⊢ (𝑦 ∈ Fin → (∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑) → ∀𝑥((♯‘𝑥) < (♯‘𝑦) → 𝜑)))
82		findcard4.3	. . . . . . . . . . 11 ⊢ (𝑦 ∈ Fin → (∀𝑥((♯‘𝑥) < (♯‘𝑦) → 𝜑) → 𝜒))
83	81, 82	syld 48	. . . . . . . . . 10 ⊢ (𝑦 ∈ Fin → (∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑) → 𝜒))
84	83	imp 412	. . . . . . . . 9 ⊢ ((𝑦 ∈ Fin ∧ ∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)) → 𝜒)
85	84	a1i 11	. . . . . . . 8 ⊢ ((card‘𝑦) = 𝑧 → ((𝑦 ∈ Fin ∧ ∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)) → 𝜒))
86	21, 50, 85	syl2and 620	. . . . . . 7 ⊢ ((card‘𝑦) = 𝑧 → ((𝑧 ∈ Fin ∧ ∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑))) → 𝜒))
87	86	com12 33	. . . . . 6 ⊢ ((𝑧 ∈ Fin ∧ ∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑))) → ((card‘𝑦) = 𝑧 → 𝜒))
88	87	alrimiv 1960	. . . . 5 ⊢ ((𝑧 ∈ Fin ∧ ∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑))) → ∀𝑦((card‘𝑦) = 𝑧 → 𝜒))
89	88	ex 418	. . . 4 ⊢ (𝑧 ∈ Fin → (∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑦((card‘𝑦) = 𝑧 → 𝜒)))
90	11, 14, 89	findcard3 9250	. . 3 ⊢ ((card‘𝐴) ∈ Fin → ∀𝑥((card‘𝑥) = (card‘𝐴) → 𝜑))
91		fveq2 6885	. . . . 5 ⊢ (𝑥 = 𝐴 → (card‘𝑥) = (card‘𝐴))
92	91	imim1i 64	. . . 4 ⊢ (((card‘𝑥) = (card‘𝐴) → 𝜑) → (𝑥 = 𝐴 → 𝜑))
93	92	alimi 1844	. . 3 ⊢ (∀𝑥((card‘𝑥) = (card‘𝐴) → 𝜑) → ∀𝑥(𝑥 = 𝐴 → 𝜑))
94	3, 90, 93	3syl 19	. 2 ⊢ (𝐴 ∈ Fin → ∀𝑥(𝑥 = 𝐴 → 𝜑))
95		nfvd 1948	. . 3 ⊢ (𝐴 ∈ Fin → Ⅎ𝑥𝜏)
96		findcard4.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
97	96	ax-gen 1828	. . . 4 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
98	97	a1i 11	. . 3 ⊢ (𝐴 ∈ Fin → ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜏)))
99		id 23	. . 3 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ Fin)
100		ceqsalt 3490	. . 3 ⊢ ((Ⅎ𝑥𝜏 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) ∧ 𝐴 ∈ Fin) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜏))
101	95, 98, 99, 100	syl3anc 1398	. 2 ⊢ (𝐴 ∈ Fin → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜏))
102	94, 101	mpbid 235	1 ⊢ (𝐴 ∈ Fin → 𝜏)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 ∀wal 1568 = wceq 1570 Ⅎwnf 1816 ∈ wcel 2146 Vcvv 3457 ⊊ wpss 3907 class class class wbr 5111 Ord word 6363 ‘cfv 6540 ωcom 7868 ≈ cen 8946 ≺ csdm 8948 Fincfn 8949 cardccrd 9937 ℝ^*cxr 11257 < clt 11258 ≤ cle 11259 ℕ₀cn0 12519 ℕ₀^*cxnn0 12592 ♯chash 14384

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-ac2 10462 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-oadd 8463 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-card 9941 df-ac 10116 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-nn 12249 df-n0 12520 df-xnn0 12593 df-z 12607 df-uz 12879 df-fz 13552 df-hash 14385

This theorem is used by: (None)

W3C validator