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 38900

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 10079	. . . 4 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
2		nnfi 9221	. . . 4 ⊢ ((card‘𝐴) ∈ ω → (card‘𝐴) ∈ Fin)
3	1, 2	syl 18	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ Fin)
4		fveq2 6916	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (card‘𝑥) = (card‘𝑦))
5	4	adantl 487	. . . . . . 7 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (card‘𝑥) = (card‘𝑦))
6		simpl 488	. . . . . . 7 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → 𝑤 = 𝑧)
7	5, 6	eqeq12d 2779	. . . . . 6 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → ((card‘𝑥) = 𝑤 ↔ (card‘𝑦) = 𝑧))
8		findcard4.1	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
9	8	adantl 487	. . . . . 6 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (𝜑 ↔ 𝜒))
10	7, 9	imbi12d 347	. . . . 5 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (((card‘𝑥) = 𝑤 → 𝜑) ↔ ((card‘𝑦) = 𝑧 → 𝜒)))
11	10	cbvaldvaw 2073	. . . 4 ⊢ (𝑤 = 𝑧 → (∀𝑥((card‘𝑥) = 𝑤 → 𝜑) ↔ ∀𝑦((card‘𝑦) = 𝑧 → 𝜒)))
12		eqeq2 2775	. . . . . 6 ⊢ (𝑤 = (card‘𝐴) → ((card‘𝑥) = 𝑤 ↔ (card‘𝑥) = (card‘𝐴)))
13	12	imbi1d 344	. . . . 5 ⊢ (𝑤 = (card‘𝐴) → (((card‘𝑥) = 𝑤 → 𝜑) ↔ ((card‘𝑥) = (card‘𝐴) → 𝜑)))
14	13	albidv 1955	. . . 4 ⊢ (𝑤 = (card‘𝐴) → (∀𝑥((card‘𝑥) = 𝑤 → 𝜑) ↔ ∀𝑥((card‘𝑥) = (card‘𝐴) → 𝜑)))
15		eleq1 2852	. . . . . . . . . 10 ⊢ ((card‘𝑦) = 𝑧 → ((card‘𝑦) ∈ Fin ↔ 𝑧 ∈ Fin))
16		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
17	16	cardid 10670	. . . . . . . . . . 11 ⊢ (card‘𝑦) ≈ 𝑦
18		enfi 9240	. . . . . . . . . . 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 4021	. . . . . . . . . . . . 13 ⊢ ((card‘𝑦) = 𝑧 → (𝑤 ⊊ (card‘𝑦) ↔ 𝑤 ⊊ 𝑧))
23	22	bicomd 226	. . . . . . . . . . . 12 ⊢ ((card‘𝑦) = 𝑧 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ (card‘𝑦)))
24	23	imbi1d 344	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → ((𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) ↔ (𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑))))
25		sp 2223	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑤 ⊊ (card‘𝑦) → 𝑤 ⊊ (card‘𝑦))
26	25	imim1i 64	. . . . . . . . . . . 12 ⊢ ((𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → (∀𝑥 𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)))
27		axi5r 2727	. . . . . . . . . . . 12 ⊢ ((∀𝑥 𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥(∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)))
28		ax-5 1945	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ⊊ (card‘𝑦) → ∀𝑥 𝑤 ⊊ (card‘𝑦))
29	28	imim1i 64	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)) → (𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)))
30		eqcom 2770	. . . . . . . . . . . . . . 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 1951	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑))))
38		ax-11 2197	. . . . . . . . . 10 ⊢ (∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)))
39	38	a1i 11	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑))))
40		nfvd 1950	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → Ⅎ𝑤((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))
41		psseq1 4020	. . . . . . . . . . . . . 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 1962	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → ∀𝑤(𝑤 = (card‘𝑥) → ((𝑤 ⊊ (card‘𝑦) → 𝜑) ↔ ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))))
45		fvexd 6931	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → (card‘𝑥) ∈ V)
46		ceqsalt 3487	. . . . . . . . . . . 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 1399	. . . . . . . . . 10 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
49	48	alimdv 1951	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
50	37, 39, 49	3syld 61	. . . . . . . 8 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥((card‘𝑥) ⊊ (card‘𝑦) → 𝜑)))
51		hashxnn0 14524	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ V → (♯‘𝑥) ∈ ℕ₀^*)
52	51	elv 3459	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘𝑥) ∈ ℕ₀^*
53		hashcl 14541	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
54		hashxrcl 14542	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ V → (♯‘𝑥) ∈ ℝ^*)
55	54	elv 3459	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘𝑥) ∈ ℝ^*
56		hashxrcl 14542	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ V → (♯‘𝑦) ∈ ℝ^*)
57	56	elv 3459	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘𝑦) ∈ ℝ^*
58		xrltle 13318	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑥) ∈ ℝ^* ∧ (♯‘𝑦) ∈ ℝ^*) → ((♯‘𝑥) < (♯‘𝑦) → (♯‘𝑥) ≤ (♯‘𝑦)))
59	55, 57, 58	mp2an 705	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑥) < (♯‘𝑦) → (♯‘𝑥) ≤ (♯‘𝑦))
60		xnn0lenn0nn0 13415	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑥) ∈ ℕ₀^* ∧ (♯‘𝑦) ∈ ℕ₀ ∧ (♯‘𝑥) ≤ (♯‘𝑦)) → (♯‘𝑥) ∈ ℕ₀)
61	52, 53, 59, 60	mp3an3an 1497	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → (♯‘𝑥) ∈ ℕ₀)
62		hashclb 14543	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ V → (𝑥 ∈ Fin ↔ (♯‘𝑥) ∈ ℕ₀))
63	62	elv 3459	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Fin ↔ (♯‘𝑥) ∈ ℕ₀)
64	61, 63	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → 𝑥 ∈ Fin)
65		hashsdom 14566	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → ((♯‘𝑥) < (♯‘𝑦) ↔ 𝑥 ≺ 𝑦))
66		cardsdom 10678	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ((card‘𝑥) ∈ (card‘𝑦) ↔ 𝑥 ≺ 𝑦))
67	66	el2v 3461	. . . . . . . . . . . . . . . . . . 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 10062	. . . . . . . . . . . . . . . 16 ⊢ (card‘𝑥) ∈ On
74	73	onordi 6502	. . . . . . . . . . . . . . 15 ⊢ Ord (card‘𝑥)
75		cardon 10062	. . . . . . . . . . . . . . . 16 ⊢ (card‘𝑦) ∈ On
76	75	onordi 6502	. . . . . . . . . . . . . . 15 ⊢ Ord (card‘𝑦)
77		ordelpss 6416	. . . . . . . . . . . . . . 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 1951	. . . . . . . . . . 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 1962	. . . . 5 ⊢ ((𝑧 ∈ Fin ∧ ∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑))) → ∀𝑦((card‘𝑦) = 𝑧 → 𝜒))
89	88	ex 418	. . . 4 ⊢ (𝑧 ∈ Fin → (∀𝑤(𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑦((card‘𝑦) = 𝑧 → 𝜒)))
90	11, 14, 89	findcard3 9312	. . 3 ⊢ ((card‘𝐴) ∈ Fin → ∀𝑥((card‘𝑥) = (card‘𝐴) → 𝜑))
91		fveq2 6916	. . . . 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 1950	. . 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 3487	. . 3 ⊢ ((Ⅎ𝑥𝜏 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) ∧ 𝐴 ∈ Fin) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜏))
101	95, 98, 99, 100	syl3anc 1399	. 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 2147 Vcvv 3454 ⊊ wpss 4016 class class class wbr 5108 Ord word 6387 ‘cfv 6566 ωcom 7911 ≈ cen 9008 ≺ csdm 9010 Fincfn 9011 cardccrd 10053 ℝ^*cxr 11381 < clt 11382 ≤ cle 11383 ℕ₀cn0 12646 ℕ₀^*cxnn0 12719 ♯chash 14515

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-ac2 10580 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-oadd 8518 df-er 8755 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-card 10057 df-ac 10234 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-nn 12376 df-n0 12647 df-xnn0 12720 df-z 12734 df-uz 13006 df-fz 13680 df-hash 14516

This theorem is used by: (None)

W3C validator