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 38739

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 10047	. . . 4 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
2		nnfi 9188	. . . 4 ⊢ ((card‘𝐴) ∈ ω → (card‘𝐴) ∈ Fin)
3	1, 2	syl 18	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ Fin)
4		fveq2 6888	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (card‘𝑥) = (card‘𝑦))
5	4	adantl 487	. . . . . . 7 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (card‘𝑥) = (card‘𝑦))
6		simpl 488	. . . . . . 7 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → 𝑤 = 𝑧)
7	5, 6	eqeq12d 2776	. . . . . 6 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → ((card‘𝑥) = 𝑤 ↔ (card‘𝑦) = 𝑧))
8		findcard4.1	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
9	8	adantl 487	. . . . . 6 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (𝜑 ↔ 𝜒))
10	7, 9	imbi12d 347	. . . . 5 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (((card‘𝑥) = 𝑤 → 𝜑) ↔ ((card‘𝑦) = 𝑧 → 𝜒)))
11	10	cbvaldvaw 2070	. . . 4 ⊢ (𝑤 = 𝑧 → (∀𝑥((card‘𝑥) = 𝑤 → 𝜑) ↔ ∀𝑦((card‘𝑦) = 𝑧 → 𝜒)))
12		eqeq2 2772	. . . . . 6 ⊢ (𝑤 = (card‘𝐴) → ((card‘𝑥) = 𝑤 ↔ (card‘𝑥) = (card‘𝐴)))
13	12	imbi1d 344	. . . . 5 ⊢ (𝑤 = (card‘𝐴) → (((card‘𝑥) = 𝑤 → 𝜑) ↔ ((card‘𝑥) = (card‘𝐴) → 𝜑)))
14	13	albidv 1952	. . . 4 ⊢ (𝑤 = (card‘𝐴) → (∀𝑥((card‘𝑥) = 𝑤 → 𝜑) ↔ ∀𝑥((card‘𝑥) = (card‘𝐴) → 𝜑)))
15		eleq1 2848	. . . . . . . . . 10 ⊢ ((card‘𝑦) = 𝑧 → ((card‘𝑦) ∈ Fin ↔ 𝑧 ∈ Fin))
16		vex 3454	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
17	16	cardid 10636	. . . . . . . . . . 11 ⊢ (card‘𝑦) ≈ 𝑦
18		enfi 9207	. . . . . . . . . . 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 4017	. . . . . . . . . . . . 13 ⊢ ((card‘𝑦) = 𝑧 → (𝑤 ⊊ (card‘𝑦) ↔ 𝑤 ⊊ 𝑧))
23	22	bicomd 226	. . . . . . . . . . . 12 ⊢ ((card‘𝑦) = 𝑧 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ (card‘𝑦)))
24	23	imbi1d 344	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → ((𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) ↔ (𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑))))
25		sp 2219	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑤 ⊊ (card‘𝑦) → 𝑤 ⊊ (card‘𝑦))
26	25	imim1i 64	. . . . . . . . . . . 12 ⊢ ((𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → (∀𝑥 𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)))
27		axi5r 2724	. . . . . . . . . . . 12 ⊢ ((∀𝑥 𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥(∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)))
28		ax-5 1942	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ⊊ (card‘𝑦) → ∀𝑥 𝑤 ⊊ (card‘𝑦))
29	28	imim1i 64	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)) → (𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)))
30		eqcom 2767	. . . . . . . . . . . . . . 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 1843	. . . . . . . . . . . 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 1948	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑))))
38		ax-11 2193	. . . . . . . . . 10 ⊢ (∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)))
39	38	a1i 11	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑))))
40		nfvd 1947	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → Ⅎ𝑤((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))
41		psseq1 4016	. . . . . . . . . . . . . 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 1959	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → ∀𝑤(𝑤 = (card‘𝑥) → ((𝑤 ⊊ (card‘𝑦) → 𝜑) ↔ ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))))
45		fvexd 6903	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → (card‘𝑥) ∈ V)
46		ceqsalt 3483	. . . . . . . . . . . 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 1948	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
50	37, 39, 49	3syld 61	. . . . . . . 8 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
51		hashxnn0 14488	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ V → (♯‘𝑥) ∈ ℕ₀^*)
52	51	elv 3455	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘𝑥) ∈ ℕ₀^*
53		hashcl 14505	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
54		hashxrcl 14506	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ V → (♯‘𝑥) ∈ ℝ^*)
55	54	elv 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘𝑥) ∈ ℝ^*
56		hashxrcl 14506	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ V → (♯‘𝑦) ∈ ℝ^*)
57	56	elv 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘𝑦) ∈ ℝ^*
58		xrltle 13283	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑥) ∈ ℝ^* ∧ (♯‘𝑦) ∈ ℝ^*) → ((♯‘𝑥) < (♯‘𝑦) → (♯‘𝑥) ≤ (♯‘𝑦)))
59	55, 57, 58	mp2an 705	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑥) < (♯‘𝑦) → (♯‘𝑥) ≤ (♯‘𝑦))
60		xnn0lenn0nn0 13380	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑥) ∈ ℕ₀^* ∧ (♯‘𝑦) ∈ ℕ₀ ∧ (♯‘𝑥) ≤ (♯‘𝑦)) → (♯‘𝑥) ∈ ℕ₀)
61	52, 53, 59, 60	mp3an3an 1496	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → (♯‘𝑥) ∈ ℕ₀)
62		hashclb 14507	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ V → (𝑥 ∈ Fin ↔ (♯‘𝑥) ∈ ℕ₀))
63	62	elv 3455	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Fin ↔ (♯‘𝑥) ∈ ℕ₀)
64	61, 63	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → 𝑥 ∈ Fin)
65		hashsdom 14530	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → ((♯‘𝑥) < (♯‘𝑦) ↔ 𝑥 ≺ 𝑦))
66		cardsdom 10644	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ((card‘𝑥) ∈ (card‘𝑦) ↔ 𝑥 ≺ 𝑦))
67	66	el2v 3457	. . . . . . . . . . . . . . . . . . 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 10030	. . . . . . . . . . . . . . . 16 ⊢ (card‘𝑥) ∈ On
74	73	onordi 6478	. . . . . . . . . . . . . . 15 ⊢ Ord (card‘𝑥)
75		cardon 10030	. . . . . . . . . . . . . . . 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 1948	. . . . . . . . . . 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 1959	. . . . 5 ⊢ ((𝑧 ∈ Fin ∧ ∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑))) → ∀𝑦((card‘𝑦) = 𝑧 → 𝜒))
89	88	ex 418	. . . 4 ⊢ (𝑧 ∈ Fin → (∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑦((card‘𝑦) = 𝑧 → 𝜒)))
90	11, 14, 89	findcard3 9279	. . 3 ⊢ ((card‘𝐴) ∈ Fin → ∀𝑥((card‘𝑥) = (card‘𝐴) → 𝜑))
91		fveq2 6888	. . . . 5 ⊢ (𝑥 = 𝐴 → (card‘𝑥) = (card‘𝐴))
92	91	imim1i 64	. . . 4 ⊢ (((card‘𝑥) = (card‘𝐴) → 𝜑) → (𝑥 = 𝐴 → 𝜑))
93	92	alimi 1843	. . 3 ⊢ (∀𝑥((card‘𝑥) = (card‘𝐴) → 𝜑) → ∀𝑥(𝑥 = 𝐴 → 𝜑))
94	3, 90, 93	3syl 19	. 2 ⊢ (𝐴 ∈ Fin → ∀𝑥(𝑥 = 𝐴 → 𝜑))
95		nfvd 1947	. . 3 ⊢ (𝐴 ∈ Fin → Ⅎ𝑥𝜏)
96		findcard4.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
97	96	ax-gen 1827	. . . 4 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
98	97	a1i 11	. . 3 ⊢ (𝐴 ∈ Fin → ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜏)))
99		id 23	. . 3 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ Fin)
100		ceqsalt 3483	. . 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 1567 = wceq 1569 Ⅎwnf 1815 ∈ wcel 2144 Vcvv 3450 ⊊ wpss 4012 class class class wbr 5102 Ord word 6363 ‘cfv 6541 ωcom 7879 ≈ cen 8975 ≺ csdm 8977 Fincfn 8978 cardccrd 10021 ℝ^*cxr 11347 < clt 11348 ≤ cle 11349 ℕ₀cn0 12611 ℕ₀^*cxnn0 12684 ♯chash 14479

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7753 ax-ac2 10546 ax-cnex 11261 ax-resscn 11262 ax-1cn 11263 ax-icn 11264 ax-addcl 11265 ax-addrcl 11266 ax-mulcl 11267 ax-mulrcl 11268 ax-mulcom 11269 ax-addass 11270 ax-mulass 11271 ax-distr 11272 ax-i2m1 11273 ax-1ne0 11274 ax-1rid 11275 ax-rnegex 11276 ax-rrecex 11277 ax-cnre 11278 ax-pre-lttri 11279 ax-pre-lttrn 11280 ax-pre-ltadd 11281 ax-pre-mulgt0 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-om 7880 df-1st 8003 df-2nd 8004 df-frecs 8304 df-wrecs 8335 df-recs 8384 df-rdg 8423 df-1o 8481 df-oadd 8485 df-er 8722 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-card 10025 df-ac 10200 df-pnf 11350 df-mnf 11351 df-xr 11352 df-ltxr 11353 df-le 11354 df-sub 11548 df-neg 11549 df-nn 12341 df-n0 12612 df-xnn0 12685 df-z 12699 df-uz 12971 df-fz 13645 df-hash 14480

This theorem is used by: (None)

W3C validator