Theorem php3 9178

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 5322. (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 8949	. . 3 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
2		bren 8930	. . . . . 6 ⊢ (𝐴 ≈ 𝑥 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝑥)
3		pssss 4063	. . . . . . . . . . . . . 14 ⊢ (𝐵 ⊊ 𝐴 → 𝐵 ⊆ 𝐴)
4		imass2 6075	. . . . . . . . . . . . . 14 ⊢ (𝐵 ⊆ 𝐴 → (𝑓 “ 𝐵) ⊆ (𝑓 “ 𝐴))
5	3, 4	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐵 ⊊ 𝐴 → (𝑓 “ 𝐵) ⊆ (𝑓 “ 𝐴))
6	5	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → (𝑓 “ 𝐵) ⊆ (𝑓 “ 𝐴))
7		pssnel 4436	. . . . . . . . . . . . . 14 ⊢ (𝐵 ⊊ 𝐴 → ∃𝑦(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
8		eldif 3926	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵))
9		f1ofn 6803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → 𝑓 Fn 𝐴)
10		difss 4101	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
11		fnfvima 7209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 Fn 𝐴 ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝑦 ∈ (𝐴 ∖ 𝐵)) → (𝑓‘𝑦) ∈ (𝑓 “ (𝐴 ∖ 𝐵)))
12	11	3expia 1121	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 Fn 𝐴 ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴) → (𝑦 ∈ (𝐴 ∖ 𝐵) → (𝑓‘𝑦) ∈ (𝑓 “ (𝐴 ∖ 𝐵))))
13	9, 10, 12	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑦 ∈ (𝐴 ∖ 𝐵) → (𝑓‘𝑦) ∈ (𝑓 “ (𝐴 ∖ 𝐵))))
14		dff1o3 6808	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝐴–1-1-onto→𝑥 ↔ (𝑓:𝐴–onto→𝑥 ∧ Fun ◡𝑓))
15		imadif 6602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun ◡𝑓 → (𝑓 “ (𝐴 ∖ 𝐵)) = ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)))
16	14, 15	simplbiim 504	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑓 “ (𝐴 ∖ 𝐵)) = ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)))
17	16	eleq2d 2815	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → ((𝑓‘𝑦) ∈ (𝑓 “ (𝐴 ∖ 𝐵)) ↔ (𝑓‘𝑦) ∈ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵))))
18	13, 17	sylibd 239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑦 ∈ (𝐴 ∖ 𝐵) → (𝑓‘𝑦) ∈ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵))))
19		n0i 4305	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓‘𝑦) ∈ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅)
20	18, 19	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑦 ∈ (𝐴 ∖ 𝐵) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅))
21	8, 20	biimtrrid 243	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → ((𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅))
22	21	exlimdv 1933	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (∃𝑦(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅))
23	22	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ ∃𝑦(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅)
24	7, 23	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → ¬ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅)
25		ssdif0 4331	. . . . . . . . . . . . 13 ⊢ ((𝑓 “ 𝐴) ⊆ (𝑓 “ 𝐵) ↔ ((𝑓 “ 𝐴) ∖ (𝑓 “ 𝐵)) = ∅)
26	24, 25	sylnibr 329	. . . . . . . . . . . 12 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → ¬ (𝑓 “ 𝐴) ⊆ (𝑓 “ 𝐵))
27		dfpss3 4054	. . . . . . . . . . . 12 ⊢ ((𝑓 “ 𝐵) ⊊ (𝑓 “ 𝐴) ↔ ((𝑓 “ 𝐵) ⊆ (𝑓 “ 𝐴) ∧ ¬ (𝑓 “ 𝐴) ⊆ (𝑓 “ 𝐵)))
28	6, 26, 27	sylanbrc 583	. . . . . . . . . . 11 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → (𝑓 “ 𝐵) ⊊ (𝑓 “ 𝐴))
29		imadmrn 6043	. . . . . . . . . . . . . 14 ⊢ (𝑓 “ dom 𝑓) = ran 𝑓
30		f1odm 6806	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → dom 𝑓 = 𝐴)
31	30	imaeq2d 6033	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑓 “ dom 𝑓) = (𝑓 “ 𝐴))
32		f1ofo 6809	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → 𝑓:𝐴–onto→𝑥)
33		forn 6777	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴–onto→𝑥 → ran 𝑓 = 𝑥)
34	32, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → ran 𝑓 = 𝑥)
35	29, 31, 34	3eqtr3a 2789	. . . . . . . . . . . . 13 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → (𝑓 “ 𝐴) = 𝑥)
36	35	psseq2d 4061	. . . . . . . . . . . 12 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → ((𝑓 “ 𝐵) ⊊ (𝑓 “ 𝐴) ↔ (𝑓 “ 𝐵) ⊊ 𝑥))
37	36	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → ((𝑓 “ 𝐵) ⊊ (𝑓 “ 𝐴) ↔ (𝑓 “ 𝐵) ⊊ 𝑥))
38	28, 37	mpbid 232	. . . . . . . . . 10 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → (𝑓 “ 𝐵) ⊊ 𝑥)
39		php2 9177	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ω ∧ (𝑓 “ 𝐵) ⊊ 𝑥) → (𝑓 “ 𝐵) ≺ 𝑥)
40	38, 39	sylan2 593	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ (𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴)) → (𝑓 “ 𝐵) ≺ 𝑥)
41		nnfi 9136	. . . . . . . . . 10 ⊢ (𝑥 ∈ ω → 𝑥 ∈ Fin)
42		f1of1 6801	. . . . . . . . . . . 12 ⊢ (𝑓:𝐴–1-1-onto→𝑥 → 𝑓:𝐴–1-1→𝑥)
43		f1ores 6816	. . . . . . . . . . . 12 ⊢ ((𝑓:𝐴–1-1→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵))
44	42, 3, 43	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → (𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵))
45		vex 3454	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
46	45	resex 6002	. . . . . . . . . . . . 13 ⊢ (𝑓 ↾ 𝐵) ∈ V
47		f1oeq1 6790	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑓 ↾ 𝐵) → (𝑦:𝐵–1-1-onto→(𝑓 “ 𝐵) ↔ (𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵)))
48	46, 47	spcev 3575	. . . . . . . . . . . 12 ⊢ ((𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵) → ∃𝑦 𝑦:𝐵–1-1-onto→(𝑓 “ 𝐵))
49		bren 8930	. . . . . . . . . . . 12 ⊢ (𝐵 ≈ (𝑓 “ 𝐵) ↔ ∃𝑦 𝑦:𝐵–1-1-onto→(𝑓 “ 𝐵))
50	48, 49	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝑓 ↾ 𝐵):𝐵–1-1-onto→(𝑓 “ 𝐵) → 𝐵 ≈ (𝑓 “ 𝐵))
51	44, 50	syl 17	. . . . . . . . . 10 ⊢ ((𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≈ (𝑓 “ 𝐵))
52		endom 8952	. . . . . . . . . . . 12 ⊢ (𝐵 ≈ (𝑓 “ 𝐵) → 𝐵 ≼ (𝑓 “ 𝐵))
53		sdomdom 8953	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 “ 𝐵) ≺ 𝑥 → (𝑓 “ 𝐵) ≼ 𝑥)
54		domfi 9158	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ Fin ∧ (𝑓 “ 𝐵) ≼ 𝑥) → (𝑓 “ 𝐵) ∈ Fin)
55	53, 54	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑓 “ 𝐵) ≺ 𝑥) → (𝑓 “ 𝐵) ∈ Fin)
56	55	3adant2 1131	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → (𝑓 “ 𝐵) ∈ Fin)
57		domfi 9158	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 “ 𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵)) → 𝐵 ∈ Fin)
58	57	3adant3 1132	. . . . . . . . . . . . . 14 ⊢ (((𝑓 “ 𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ∈ Fin)
59		domsdomtrfi 9171	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ≺ 𝑥)
60	58, 59	syld3an1 1412	. . . . . . . . . . . . 13 ⊢ (((𝑓 “ 𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ≺ 𝑥)
61	56, 60	syld3an1 1412	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ≺ 𝑥)
62	52, 61	syl3an2 1164	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≈ (𝑓 “ 𝐵) ∧ (𝑓 “ 𝐵) ≺ 𝑥) → 𝐵 ≺ 𝑥)
63	62	3expia 1121	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≈ (𝑓 “ 𝐵)) → ((𝑓 “ 𝐵) ≺ 𝑥 → 𝐵 ≺ 𝑥))
64	41, 51, 63	syl2an 596	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ (𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴)) → ((𝑓 “ 𝐵) ≺ 𝑥 → 𝐵 ≺ 𝑥))
65	40, 64	mpd 15	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑓:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊊ 𝐴)) → 𝐵 ≺ 𝑥)
66	65	exp32 420	. . . . . . 7 ⊢ (𝑥 ∈ ω → (𝑓:𝐴–1-1-onto→𝑥 → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥)))
67	66	exlimdv 1933	. . . . . 6 ⊢ (𝑥 ∈ ω → (∃𝑓 𝑓:𝐴–1-1-onto→𝑥 → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥)))
68	2, 67	biimtrid 242	. . . . 5 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝑥)))
69		ensymfib 9153	. . . . . . . . . . 11 ⊢ (𝑥 ∈ Fin → (𝑥 ≈ 𝐴 ↔ 𝐴 ≈ 𝑥))
70	69	adantr 480	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥) → (𝑥 ≈ 𝐴 ↔ 𝐴 ≈ 𝑥))
71	70	biimp3ar 1472	. . . . . . . . 9 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝐴 ≈ 𝑥) → 𝑥 ≈ 𝐴)
72		endom 8952	. . . . . . . . . 10 ⊢ (𝑥 ≈ 𝐴 → 𝑥 ≼ 𝐴)
73		sdomdom 8953	. . . . . . . . . . . . 13 ⊢ (𝐵 ≺ 𝑥 → 𝐵 ≼ 𝑥)
74		domfi 9158	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ 𝑥) → 𝐵 ∈ Fin)
75	73, 74	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥) → 𝐵 ∈ Fin)
76	75	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≼ 𝐴) → 𝐵 ∈ Fin)
77		sdomdomtrfi 9170	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≼ 𝐴) → 𝐵 ≺ 𝐴)
78	76, 77	syld3an1 1412	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≼ 𝐴) → 𝐵 ≺ 𝐴)
79	72, 78	syl3an3 1165	. . . . . . . . 9 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝑥 ≈ 𝐴) → 𝐵 ≺ 𝐴)
80	71, 79	syld3an3 1411	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≺ 𝑥 ∧ 𝐴 ≈ 𝑥) → 𝐵 ≺ 𝐴)
81	41, 80	syl3an1 1163	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝐵 ≺ 𝑥 ∧ 𝐴 ≈ 𝑥) → 𝐵 ≺ 𝐴)
82	81	3com23 1126	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥 ∧ 𝐵 ≺ 𝑥) → 𝐵 ≺ 𝐴)
83	82	3exp 1119	. . . . 5 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ≺ 𝑥 → 𝐵 ≺ 𝐴)))
84	68, 83	syldd 72	. . . 4 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ⊊ 𝐴 → 𝐵 ≺ 𝐴)))
85	84	rexlimiv 3128	. . 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 1540  ∃wex 1779   ∈ wcel 2109  ∃wrex 3054   ∖ cdif 3913   ⊆ wss 3916   ⊊ wpss 3917  ∅c0 4298   class class class wbr 5109  ^◡ccnv 5639  dom cdm 5640  ran crn 5641   ↾ cres 5642   “ cima 5643  Fun wfun 6507   Fn wfn 6508  –1-1→wf1 6510  –onto→wfo 6511  –1-1-onto→wf1o 6512  ‘cfv 6513  ωcom 7844   ≈ cen 8917   ≼ cdom 8918   ≺ csdm 8919  Fincfn 8920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389  ax-un 7713

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-pss 3936  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-ord 6337  df-on 6338  df-lim 6339  df-suc 6340  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-om 7845  df-1o 8436  df-en 8921  df-dom 8922  df-sdom 8923  df-fin 8924

This theorem is referenced by:  phpeqd  9181  onomeneq  9183  pssinf  9209  f1finf1o  9222  f1finf1oOLD  9223  findcard3  9235  findcard3OLD  9236  fofinf1o  9289  ackbij1b  10197  fincssdom  10282  fin23lem25  10283  canthp1lem2  10612  pwfseqlem4  10621  uzindi  13953  symggen  19406  pgpssslw  19550  pgpfaclem2  20020  ppiltx  27093  finminlem  36301  lindsenlbs  37604