Theorem php3 9143

Description: Corollary of Pigeonhole Principle. If 𝐴 is finite and 𝐵 is a proper subset of 𝐴, the 𝐵 is strictly less numerous than 𝐴. Stronger version of Corollary 6C of [Enderton] p. 135. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5307. (Revised by BTernaryTau, 26-Nov-2024.)

Assertion

Ref	Expression
php3	⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)

Proof of Theorem php3

Dummy variables 𝑓 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 8922	. . 3 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
2		bren 8903	. . . . . 6 ⊢ (𝐴 ≈ 𝑥 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝑥)
3		pssss 4038	. . . . . . . . . . . . . 14 ⊢ (𝐵 ⊊ 𝐴 → 𝐵 ⊆ 𝐴)
4		imass2 6067	. . . . . . . . . . . . . 14 ⊢ (𝐵 ⊆ 𝐴 → (𝑓 “ 𝐵) ⊆ (𝑓 “ 𝐴))
5	3, 4	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐵 ⊊ 𝐴 → (𝑓 “ 𝐵) ⊆ (𝑓 “ 𝐴))
6	5	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → (𝑓 “ 𝐵) ⊆ (𝑓 “ 𝐴))
7		pssnel 4411	. . . . . . . . . . . . . 14 ⊢ (𝐵 ⊊ 𝐴 → ∃𝑦(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
8		eldif 3899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
9		f1ofn 6781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → 𝑓 Fn 𝐴)
10		difss 4076	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
11		fnfvima 7188	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 Fn 𝐴 ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝑦 ∈ (𝐴 ∖ 𝐵)) → (𝑓‘𝑦) ∈ (𝑓 “ (𝐴 ∖ 𝐵)))
12	11	3expia 1122	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 Fn 𝐴 ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴) → (𝑦 ∈ (𝐴 ∖ 𝐵) → (𝑓‘𝑦) ∈ (𝑓 “ (𝐴 ∖ 𝐵))))
13	9, 10, 12	sylancl 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑦 ∈ (𝐴 ∖ 𝐵) → (𝑓‘𝑦) ∈ (𝑓 “ (𝐴 ∖ 𝐵))))
14		dff1o3 6786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝐴–1-1-onto→𝑥 ↔ (𝑓:𝐴–onto→𝑥 ∧ Fun ◡𝑓))
15		imadif 6582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun ◡𝑓 → (𝑓 “ (𝐴 ∖ 𝐵)) = ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)))
16	14, 15	simplbiim 504	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑓 “ (𝐴 ∖ 𝐵)) = ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)))
17	16	eleq2d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → ((𝑓‘𝑦) ∈ (𝑓 “ (𝐴 ∖ 𝐵)) ↔ (𝑓‘𝑦) ∈ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵))))
18	13, 17	sylibd 239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑦 ∈ (𝐴 ∖ 𝐵) → (𝑓‘𝑦) ∈ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵))))
19		n0i 4280	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓‘𝑦) ∈ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅)
20	18, 19	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑦 ∈ (𝐴 ∖ 𝐵) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅))
21	8, 20	biimtrrid 243	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → ((𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅))
22	21	exlimdv 1935	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (∃𝑦(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅))
23	22	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ ∃𝑦(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅)
24	7, 23	sylan2 594	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅)
25		ssdif0 4306	. . . . . . . . . . . . 13 ⊢ ((𝑓 “ 𝐴) ⊆ (𝑓 “ 𝐵) ↔ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅)
26	24, 25	sylnibr 329	. . . . . . . . . . . 12 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → ¬ (𝑓 “ 𝐴) ⊆ (𝑓 “ 𝐵))
27		dfpss3 4029	. . . . . . . . . . . 12 ⊢ ((𝑓 “ 𝐵) ⊊ (𝑓 “ 𝐴) ↔ ((𝑓 “ 𝐵) ⊆ (𝑓 “ 𝐴) ∧ ¬ (𝑓 “ 𝐴) ⊆ (𝑓 “ 𝐵)))
28	6, 26, 27	sylanbrc 584	. . . . . . . . . . 11 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → (𝑓 “ 𝐵) ⊊ (𝑓 “ 𝐴))
29		imadmrn 6035	. . . . . . . . . . . . . 14 ⊢ (𝑓 “ dom 𝑓) = ran 𝑓
30		f1odm 6784	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → dom 𝑓 = 𝐴)
31	30	imaeq2d 6025	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑓 “ dom 𝑓) = (𝑓 “ 𝐴))
32		f1ofo 6787	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → 𝑓:𝐴–onto→𝑥)
33		forn 6755	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴–onto→𝑥 → ran 𝑓 = 𝑥)
34	32, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → ran 𝑓 = 𝑥)
35	29, 31, 34	3eqtr3a 2795	. . . . . . . . . . . . 13 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑓 “ 𝐴) = 𝑥)
36	35	psseq2d 4036	. . . . . . . . . . . 12 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → ((𝑓 “ 𝐵) ⊊ (𝑓 “ 𝐴) ↔ (𝑓 “ 𝐵) ⊊ 𝑥))
37	36	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → ((𝑓 “ 𝐵) ⊊ (𝑓 “ 𝐴) ↔ (𝑓 “ 𝐵) ⊊ 𝑥))
38	28, 37	mpbid 232	. . . . . . . . . 10 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → (𝑓 “ 𝐵) ⊊ 𝑥)
39		php2 9142	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ω ∧ (𝑓 “ 𝐵) ⊊ 𝑥) → (𝑓 “ 𝐵) ≺ 𝑥)
40	38, 39	sylan2 594	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ (𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴)) → (𝑓 “ 𝐵) ≺ 𝑥)
41		nnfi 9102	. . . . . . . . . 10 ⊢ (𝑥 ∈ ω → 𝑥 ∈ Fin)
42		f1of1 6779	. . . . . . . . . . . 12 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → 𝑓:𝐴–1-1→𝑥)
43		f1ores 6794	. . . . . . . . . . . 12 ⊢ ((𝑓:𝐴–1-1→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵))
44	42, 3, 43	syl2an 597	. . . . . . . . . . 11 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → (𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵))
45		vex 3433	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
46	45	resex 5994	. . . . . . . . . . . . 13 ⊢ (𝑓 ↾ 𝐵) ∈ V
47		f1oeq1 6768	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑓 ↾ 𝐵) → (𝑦:𝐵–1-1-onto→(𝑓 “ 𝐵) ↔ (𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵)))
48	46, 47	spcev 3548	. . . . . . . . . . . 12 ⊢ ((𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵) → ∃𝑦 𝑦:𝐵–1-1-onto→(𝑓 “ 𝐵))
49		bren 8903	. . . . . . . . . . . 12 ⊢ (𝐵 ≈ (𝑓 “ 𝐵) ↔ ∃𝑦 𝑦:𝐵–1-1-onto→(𝑓 “ 𝐵))
50	48, 49	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵) → 𝐵 ≈ (𝑓 “ 𝐵))
51	44, 50	syl 17	. . . . . . . . . 10 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≈ (𝑓 “ 𝐵))
52		endom 8926	. . . . . . . . . . . 12 ⊢ (𝐵 ≈ (𝑓 “ 𝐵) → 𝐵 ≼ (𝑓 “ 𝐵))
53		sdomdom 8927	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 “ 𝐵) ≺ 𝑥 → (𝑓 “ 𝐵) ≼ 𝑥)
54		domfi 9123	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ Fin ∧ (𝑓 “ 𝐵) ≼ 𝑥) → (𝑓 “ 𝐵) ∈ Fin)
55	53, 54	sylan2 594	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑓 “ 𝐵) ≺ 𝑥) → (𝑓 “ 𝐵) ∈ Fin)
56	55	3adant2 1132	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → (𝑓 “ 𝐵) ∈ Fin)
57		domfi 9123	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 “ 𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵)) → 𝐵 ∈ Fin)
58	57	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ (((𝑓 “ 𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ∈ Fin)
59		domsdomtrfi 9136	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ≺ 𝑥)
60	58, 59	syld3an1 1413	. . . . . . . . . . . . 13 ⊢ (((𝑓 “ 𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ≺ 𝑥)
61	56, 60	syld3an1 1413	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ≺ 𝑥)
62	52, 61	syl3an2 1165	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≈ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ≺ 𝑥)
63	62	3expia 1122	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≈ (𝑓 “ 𝐵)) → ((𝑓 “ 𝐵) ≺ 𝑥 → 𝐵 ≺ 𝑥))
64	41, 51, 63	syl2an 597	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ (𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴)) → ((𝑓 “ 𝐵) ≺ 𝑥 → 𝐵 ≺ 𝑥))
65	40, 64	mpd 15	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴)) → 𝐵 ≺ 𝑥)
66	65	exp32 420	. . . . . . 7 ⊢ (𝑥 ∈ ω → (𝑓:𝐴–1-1-onto→𝑥 → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥)))
67	66	exlimdv 1935	. . . . . 6 ⊢ (𝑥 ∈ ω → (∃𝑓 𝑓:𝐴–1-1-onto→𝑥 → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥)))
68	2, 67	biimtrid 242	. . . . 5 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥)))
69		ensymfib 9118	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Fin → (𝑥 ≈ 𝐴 ↔ 𝐴 ≈ 𝑥))
70	69	adantr 480	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥) → (𝑥 ≈ 𝐴 ↔ 𝐴 ≈ 𝑥))
71	70	biimp3ar 1473	. . . . . . . . 9 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝐴 ≈ 𝑥) → 𝑥 ≈ 𝐴)
72		endom 8926	. . . . . . . . . 10 ⊢ (𝑥 ≈ 𝐴 → 𝑥 ≼ 𝐴)
73		sdomdom 8927	. . . . . . . . . . . . 13 ⊢ (𝐵 ≺ 𝑥 → 𝐵 ≼ 𝑥)
74		domfi 9123	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ 𝑥) → 𝐵 ∈ Fin)
75	73, 74	sylan2 594	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥) → 𝐵 ∈ Fin)
76	75	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≼ 𝐴) → 𝐵 ∈ Fin)
77		sdomdomtrfi 9135	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≼ 𝐴) → 𝐵 ≺ 𝐴)
78	76, 77	syld3an1 1413	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≼ 𝐴) → 𝐵 ≺ 𝐴)
79	72, 78	syl3an3 1166	. . . . . . . . 9 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≈ 𝐴) → 𝐵 ≺ 𝐴)
80	71, 79	syld3an3 1412	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝐴 ≈ 𝑥) → 𝐵 ≺ 𝐴)
81	41, 80	syl3an1 1164	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝐵 ≺ 𝑥 ∧ 𝐴 ≈ 𝑥) → 𝐵 ≺ 𝐴)
82	81	3com23 1127	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥 ∧ 𝐵 ≺ 𝑥) → 𝐵 ≺ 𝐴)
83	82	3exp 1120	. . . . 5 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ≺ 𝑥 → 𝐵 ≺ 𝐴)))
84	68, 83	syldd 72	. . . 4 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴)))
85	84	rexlimiv 3131	. . 3 ⊢ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴))
86	1, 85	sylbi 217	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴))
87	86	imp 406	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061   ∖ cdif 3886   ⊆ wss 3889   ⊊ wpss 3890  ∅c0 4273   class class class wbr 5085  ^◡ccnv 5630  dom cdm 5631  ran crn 5632   ↾ cres 5633   “ cima 5634  Fun wfun 6492   Fn wfn 6493  –1-1→wf1 6495  –onto→wfo 6496  –1-1-onto→wf1o 6497  ‘cfv 6498  ωcom 7817   ≈ cen 8890   ≼ cdom 8891   ≺ csdm 8892  Fincfn 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-om 7818  df-1o 8405  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897

This theorem is referenced by:  phpeqd  9146  onomeneq  9148  pssinf  9172  f1finf1o  9183  findcard3  9193  fofinf1o  9242  ackbij1b  10160  fincssdom  10245  fin23lem25  10246  canthp1lem2  10576  pwfseqlem4  10585  uzindi  13944  symggen  19445  pgpssslw  19589  pgpfaclem2  20059  ppiltx  27140  finminlem  36500  lindsenlbs  37936