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 38612

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 10035	. . . 4 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
2		nnfi 9176	. . . 4 ⊢ ((card‘𝐴) ∈ ω → (card‘𝐴) ∈ Fin)
3	1, 2	syl 18	. . 3 ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ Fin)
4		fveq2 6883	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (card‘𝑥) = (card‘𝑦))
5	4	adantl 487	. . . . . . 7 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → (card‘𝑥) = (card‘𝑦))
6		simpl 488	. . . . . . 7 ⊢ ((𝑤 = 𝑧 ∧ 𝑥 = 𝑦) → 𝑤 = 𝑧)
7	5, 6	eqeq12d 2777	. . . . . 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 2773	. . . . . 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 2849	. . . . . . . . . 10 ⊢ ((card‘𝑦) = 𝑧 → ((card‘𝑦) ∈ Fin ↔ 𝑧 ∈ Fin))
16		vex 3455	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
17	16	cardid 10624	. . . . . . . . . . 11 ⊢ (card‘𝑦) ≈ 𝑦
18		enfi 9195	. . . . . . . . . . 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 4039	. . . . . . . . . . . . 13 ⊢ ((card‘𝑦) = 𝑧 → (𝑤 ⊊ (card‘𝑦) ↔ 𝑤 ⊊ 𝑧))
23	22	bicomd 226	. . . . . . . . . . . 12 ⊢ ((card‘𝑦) = 𝑧 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ (card‘𝑦)))
24	23	imbi1d 344	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → ((𝑤 ⊊ 𝑧 → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) ↔ (𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑))))
25		sp 2220	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑤 ⊊ (card‘𝑦) → 𝑤 ⊊ (card‘𝑦))
26	25	imim1i 64	. . . . . . . . . . . 12 ⊢ ((𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → (∀𝑥 𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)))
27		axi5r 2725	. . . . . . . . . . . 12 ⊢ ((∀𝑥 𝑤 ⊊ (card‘𝑦) → ∀𝑥((card‘𝑥) = 𝑤 → 𝜑)) → ∀𝑥(∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)))
28		ax-5 1943	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ⊊ (card‘𝑦) → ∀𝑥 𝑤 ⊊ (card‘𝑦))
29	28	imim1i 64	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)) → (𝑤 ⊊ (card‘𝑦) → ((card‘𝑥) = 𝑤 → 𝜑)))
30		eqcom 2768	. . . . . . . . . . . . . . 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 2194	. . . . . . . . . 10 ⊢ (∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)))
39	38	a1i 11	. . . . . . . . 9 ⊢ ((card‘𝑦) = 𝑧 → (∀𝑤∀𝑥(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑)) → ∀𝑥∀𝑤(𝑤 = (card‘𝑥) → (𝑤 ⊊ (card‘𝑦) → 𝜑))))
40		nfvd 1948	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → Ⅎ𝑤((card‘𝑥) ⊊ (card‘𝑦) → 𝜑))
41		psseq1 4038	. . . . . . . . . . . . . 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 6898	. . . . . . . . . . 11 ⊢ ((card‘𝑦) = 𝑧 → (card‘𝑥) ∈ V)
46		ceqsalt 3484	. . . . . . . . . . . 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 14476	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ V → (♯‘𝑥) ∈ ℕ₀^*)
52	51	elv 3456	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘𝑥) ∈ ℕ₀^*
53		hashcl 14493	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
54		hashxrcl 14494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ V → (♯‘𝑥) ∈ ℝ^*)
55	54	elv 3456	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘𝑥) ∈ ℝ^*
56		hashxrcl 14494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ V → (♯‘𝑦) ∈ ℝ^*)
57	56	elv 3456	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘𝑦) ∈ ℝ^*
58		xrltle 13271	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑥) ∈ ℝ^* ∧ (♯‘𝑦) ∈ ℝ^*) → ((♯‘𝑥) < (♯‘𝑦) → (♯‘𝑥) ≤ (♯‘𝑦)))
59	55, 57, 58	mp2an 705	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑥) < (♯‘𝑦) → (♯‘𝑥) ≤ (♯‘𝑦))
60		xnn0lenn0nn0 13368	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑥) ∈ ℕ₀^* ∧ (♯‘𝑦) ∈ ℕ₀ ∧ (♯‘𝑥) ≤ (♯‘𝑦)) → (♯‘𝑥) ∈ ℕ₀)
61	52, 53, 59, 60	mp3an3an 1496	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → (♯‘𝑥) ∈ ℕ₀)
62		hashclb 14495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ V → (𝑥 ∈ Fin ↔ (♯‘𝑥) ∈ ℕ₀))
63	62	elv 3456	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Fin ↔ (♯‘𝑥) ∈ ℕ₀)
64	61, 63	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Fin ∧ (♯‘𝑥) < (♯‘𝑦)) → 𝑥 ∈ Fin)
65		hashsdom 14518	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → ((♯‘𝑥) < (♯‘𝑦) ↔ 𝑥 ≺ 𝑦))
66		cardsdom 10632	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ((card‘𝑥) ∈ (card‘𝑦) ↔ 𝑥 ≺ 𝑦))
67	66	el2v 3458	. . . . . . . . . . . . . . . . . . 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 10018	. . . . . . . . . . . . . . . 16 ⊢ (card‘𝑥) ∈ On
74	73	onordi 6475	. . . . . . . . . . . . . . 15 ⊢ Ord (card‘𝑥)
75		cardon 10018	. . . . . . . . . . . . . . . 16 ⊢ (card‘𝑦) ∈ On
76	75	onordi 6475	. . . . . . . . . . . . . . 15 ⊢ Ord (card‘𝑦)
77		ordelpss 6389	. . . . . . . . . . . . . . 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 9267	. . 3 ⊢ ((card‘𝐴) ∈ Fin → ∀𝑥((card‘𝑥) = (card‘𝐴) → 𝜑))
91		fveq2 6883	. . . . 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 3484	. . 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 2145 Vcvv 3451 ⊊ wpss 3900 class class class wbr 5103 Ord word 6360 ‘cfv 6537 ωcom 7875 ≈ cen 8963 ≺ csdm 8965 Fincfn 8966 cardccrd 10009 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 ℕ₀cn0 12599 ℕ₀^*cxnn0 12672 ♯chash 14467

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-ac2 10534 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-oadd 8473 df-er 8710 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-card 10013 df-ac 10188 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-nn 12329 df-n0 12600 df-xnn0 12673 df-z 12687 df-uz 12959 df-fz 13633 df-hash 14468

This theorem is used by: (None)

W3C validator