Theorem weexenwe

Description: If a well-ordering of an infinite set exists, then a well-ordering equinumerous to the set exists. (Contributed by BTernaryTau, 31-Jul-2026)

	Ref	Expression
Assertion	weexenwe	⊢ ( ( ∃ 𝑟 𝑟 We 𝐴 ∧ ω ≼ 𝐴 ) → ∃ 𝑠 ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ween	⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑟 𝑟 We 𝐴 )
2		inss2	⊢ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )
3		weinxp	⊢ ( 𝑟 We 𝐴 ↔ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
4	3	biimpi	⊢ ( 𝑟 We 𝐴 → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
5	4	3ad2ant3	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝑟 We 𝐴 ) → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 )
6		reldom	⊢ Rel ≼
7	6	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
8	7 7	xpexd	⊢ ( ω ≼ 𝐴 → ( 𝐴 × 𝐴 ) ∈ V )
9		ssdomg	⊢ ( ( 𝐴 × 𝐴 ) ∈ V → ( ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≼ ( 𝐴 × 𝐴 ) ) )
10	8 2 9	mpisyl	⊢ ( ω ≼ 𝐴 → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≼ ( 𝐴 × 𝐴 ) )
11		infxpidm2	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
12		domentr	⊢ ( ( ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≼ ( 𝐴 × 𝐴 ) ∧ ( 𝐴 × 𝐴 ) ≈ 𝐴 ) → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≼ 𝐴 )
13	10 11 12	syl2an2	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≼ 𝐴 )
14	13	3adant3	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝑟 We 𝐴 ) → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≼ 𝐴 )
15		weso	⊢ ( ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) Or 𝐴 )
16	3 15	sylbi	⊢ ( 𝑟 We 𝐴 → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) Or 𝐴 )
17		vex	⊢ 𝑟 ∈ V
18	17	inex1	⊢ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ∈ V
19		soinfdom	⊢ ( ( ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) Or 𝐴 ∧ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ∈ V ∧ ω ≼ 𝐴 ) → 𝐴 ≼ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) )
20	18 19	mp3an2	⊢ ( ( ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) Or 𝐴 ∧ ω ≼ 𝐴 ) → 𝐴 ≼ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) )
21	16 20	sylan	⊢ ( ( 𝑟 We 𝐴 ∧ ω ≼ 𝐴 ) → 𝐴 ≼ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) )
22	21	ancoms	⊢ ( ( ω ≼ 𝐴 ∧ 𝑟 We 𝐴 ) → 𝐴 ≼ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) )
23	22	3adant1	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝑟 We 𝐴 ) → 𝐴 ≼ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) )
24		sbth	⊢ ( ( ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≼ 𝐴 ∧ 𝐴 ≼ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ) → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≈ 𝐴 )
25	14 23 24	syl2anc	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝑟 We 𝐴 ) → ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≈ 𝐴 )
26		sseq1	⊢ ( 𝑠 = ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ↔ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) ) )
27		weeq1	⊢ ( 𝑠 = ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑠 We 𝐴 ↔ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ) )
28		breq1	⊢ ( 𝑠 = ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑠 ≈ 𝐴 ↔ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≈ 𝐴 ) )
29	26 27 28	3anbi123d	⊢ ( 𝑠 = ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) → ( ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴 ) ↔ ( ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) ∧ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ∧ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≈ 𝐴 ) ) )
30	18 29	spcev	⊢ ( ( ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) ∧ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) We 𝐴 ∧ ( 𝑟 ∩ ( 𝐴 × 𝐴 ) ) ≈ 𝐴 ) → ∃ 𝑠 ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴 ) )
31	2 5 25 30	mp3an2i	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝑟 We 𝐴 ) → ∃ 𝑠 ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴 ) )
32	31	3expia	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝑟 We 𝐴 → ∃ 𝑠 ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴 ) ) )
33	32	exlimdv	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ∃ 𝑟 𝑟 We 𝐴 → ∃ 𝑠 ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴 ) ) )
34	1 33	sylanbr	⊢ ( ( ∃ 𝑟 𝑟 We 𝐴 ∧ ω ≼ 𝐴 ) → ( ∃ 𝑟 𝑟 We 𝐴 → ∃ 𝑠 ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴 ) ) )
35	34	adantrd	⊢ ( ( ∃ 𝑟 𝑟 We 𝐴 ∧ ω ≼ 𝐴 ) → ( ( ∃ 𝑟 𝑟 We 𝐴 ∧ ω ≼ 𝐴 ) → ∃ 𝑠 ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴 ) ) )
36	35	pm2.43i	⊢ ( ( ∃ 𝑟 𝑟 We 𝐴 ∧ ω ≼ 𝐴 ) → ∃ 𝑠 ( 𝑠 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴 ) )