Theorem safesnsupfidom1o

Description: If B is a finite subset of ordered class A , we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024)

	Ref	Expression
Hypotheses	safesnsupfidom1o.small	⊢ ( 𝜑 → ( 𝑂 = ∅ ∨ 𝑂 = 1o ) )
	safesnsupfidom1o.finite	⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion	safesnsupfidom1o	⊢ ( 𝜑 → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ≼ 1o )

Proof

Step	Hyp	Ref	Expression
1		safesnsupfidom1o.small	⊢ ( 𝜑 → ( 𝑂 = ∅ ∨ 𝑂 = 1o ) )
2		safesnsupfidom1o.finite	⊢ ( 𝜑 → 𝐵 ∈ Fin )
3		iftrue	⊢ ( 𝑂 ≺ 𝐵 → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) = { sup ( 𝐵 , 𝐴 , 𝑅 ) } )
4	3	adantl	⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) = { sup ( 𝐵 , 𝐴 , 𝑅 ) } )
5		ensn1g	⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ V → { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≈ 1o )
6		1on	⊢ 1o ∈ On
7		domrefg	⊢ ( 1o ∈ On → 1o ≼ 1o )
8	6 7	ax-mp	⊢ 1o ≼ 1o
9		endomtr	⊢ ( ( { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≈ 1o ∧ 1o ≼ 1o ) → { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≼ 1o )
10	5 8 9	sylancl	⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ V → { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≼ 1o )
11		snprc	⊢ ( ¬ sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ V ↔ { sup ( 𝐵 , 𝐴 , 𝑅 ) } = ∅ )
12		snex	⊢ { sup ( 𝐵 , 𝐴 , 𝑅 ) } ∈ V
13		eqeng	⊢ ( { sup ( 𝐵 , 𝐴 , 𝑅 ) } ∈ V → ( { sup ( 𝐵 , 𝐴 , 𝑅 ) } = ∅ → { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≈ ∅ ) )
14	12 13	ax-mp	⊢ ( { sup ( 𝐵 , 𝐴 , 𝑅 ) } = ∅ → { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≈ ∅ )
15	11 14	sylbi	⊢ ( ¬ sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ V → { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≈ ∅ )
16		0domg	⊢ ( 1o ∈ On → ∅ ≼ 1o )
17	6 16	ax-mp	⊢ ∅ ≼ 1o
18		endomtr	⊢ ( ( { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≈ ∅ ∧ ∅ ≼ 1o ) → { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≼ 1o )
19	15 17 18	sylancl	⊢ ( ¬ sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ V → { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≼ 1o )
20	10 19	pm2.61i	⊢ { sup ( 𝐵 , 𝐴 , 𝑅 ) } ≼ 1o
21	4 20	eqbrtrdi	⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ≼ 1o )
22		iffalse	⊢ ( ¬ 𝑂 ≺ 𝐵 → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) = 𝐵 )
23	22	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑂 ≺ 𝐵 ) → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) = 𝐵 )
24		0elon	⊢ ∅ ∈ On
25		eleq1	⊢ ( 𝑂 = ∅ → ( 𝑂 ∈ On ↔ ∅ ∈ On ) )
26	24 25	mpbiri	⊢ ( 𝑂 = ∅ → 𝑂 ∈ On )
27		eleq1	⊢ ( 𝑂 = 1o → ( 𝑂 ∈ On ↔ 1o ∈ On ) )
28	6 27	mpbiri	⊢ ( 𝑂 = 1o → 𝑂 ∈ On )
29	26 28	jaoi	⊢ ( ( 𝑂 = ∅ ∨ 𝑂 = 1o ) → 𝑂 ∈ On )
30		fidomtri	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑂 ∈ On ) → ( 𝐵 ≼ 𝑂 ↔ ¬ 𝑂 ≺ 𝐵 ) )
31	29 30	sylan2	⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑂 = ∅ ∨ 𝑂 = 1o ) ) → ( 𝐵 ≼ 𝑂 ↔ ¬ 𝑂 ≺ 𝐵 ) )
32		breq2	⊢ ( 𝑂 = ∅ → ( 𝐵 ≼ 𝑂 ↔ 𝐵 ≼ ∅ ) )
33		domtr	⊢ ( ( 𝐵 ≼ ∅ ∧ ∅ ≼ 1o ) → 𝐵 ≼ 1o )
34	17 33	mpan2	⊢ ( 𝐵 ≼ ∅ → 𝐵 ≼ 1o )
35	32 34	biimtrdi	⊢ ( 𝑂 = ∅ → ( 𝐵 ≼ 𝑂 → 𝐵 ≼ 1o ) )
36		breq2	⊢ ( 𝑂 = 1o → ( 𝐵 ≼ 𝑂 ↔ 𝐵 ≼ 1o ) )
37	36	biimpd	⊢ ( 𝑂 = 1o → ( 𝐵 ≼ 𝑂 → 𝐵 ≼ 1o ) )
38	35 37	jaoi	⊢ ( ( 𝑂 = ∅ ∨ 𝑂 = 1o ) → ( 𝐵 ≼ 𝑂 → 𝐵 ≼ 1o ) )
39	38	adantl	⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑂 = ∅ ∨ 𝑂 = 1o ) ) → ( 𝐵 ≼ 𝑂 → 𝐵 ≼ 1o ) )
40	31 39	sylbird	⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑂 = ∅ ∨ 𝑂 = 1o ) ) → ( ¬ 𝑂 ≺ 𝐵 → 𝐵 ≼ 1o ) )
41	2 1 40	syl2anc	⊢ ( 𝜑 → ( ¬ 𝑂 ≺ 𝐵 → 𝐵 ≼ 1o ) )
42	41	imp	⊢ ( ( 𝜑 ∧ ¬ 𝑂 ≺ 𝐵 ) → 𝐵 ≼ 1o )
43	23 42	eqbrtrd	⊢ ( ( 𝜑 ∧ ¬ 𝑂 ≺ 𝐵 ) → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ≼ 1o )
44	21 43	pm2.61dan	⊢ ( 𝜑 → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ≼ 1o )