Theorem noetalem2

Description: Lemma for noeta . The full statement of the theorem with hypotheses in place. (Contributed by Scott Fenton, 10-Aug-2024)

	Ref	Expression
Hypotheses	noetalem2.1	⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
	noetalem2.2	⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion	noetalem2	⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ∃ 𝑐 ∈ No ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ∧ ( bday ‘ 𝑐 ) ⊆ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		noetalem2.1	⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2		noetalem2.2	⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
3		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
4	3	anim2i	⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
5		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
6	5	anim2i	⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) )
7		id	⊢ ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 )
8	4 6 7	3anim123i	⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) → ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) )
9		eqid	⊢ ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) = ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
10		eqid	⊢ ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ) = ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) )
11	1 2 9 10	noetalem1	⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ( ( 𝑆 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) ∨ ( 𝑇 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) ) )
12		breq2	⊢ ( 𝑐 = 𝑆 → ( 𝑎 <s 𝑐 ↔ 𝑎 <s 𝑆 ) )
13	12	ralbidv	⊢ ( 𝑐 = 𝑆 → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ↔ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ) )
14		breq1	⊢ ( 𝑐 = 𝑆 → ( 𝑐 <s 𝑏 ↔ 𝑆 <s 𝑏 ) )
15	14	ralbidv	⊢ ( 𝑐 = 𝑆 → ( ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ) )
16		fveq2	⊢ ( 𝑐 = 𝑆 → ( bday ‘ 𝑐 ) = ( bday ‘ 𝑆 ) )
17	16	sseq1d	⊢ ( 𝑐 = 𝑆 → ( ( bday ‘ 𝑐 ) ⊆ 𝑂 ↔ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) )
18	13 15 17	3anbi123d	⊢ ( 𝑐 = 𝑆 → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ∧ ( bday ‘ 𝑐 ) ⊆ 𝑂 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) )
19	18	rspcev	⊢ ( ( 𝑆 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) → ∃ 𝑐 ∈ No ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ∧ ( bday ‘ 𝑐 ) ⊆ 𝑂 ) )
20		breq2	⊢ ( 𝑐 = 𝑇 → ( 𝑎 <s 𝑐 ↔ 𝑎 <s 𝑇 ) )
21	20	ralbidv	⊢ ( 𝑐 = 𝑇 → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ↔ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ) )
22		breq1	⊢ ( 𝑐 = 𝑇 → ( 𝑐 <s 𝑏 ↔ 𝑇 <s 𝑏 ) )
23	22	ralbidv	⊢ ( 𝑐 = 𝑇 → ( ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ) )
24		fveq2	⊢ ( 𝑐 = 𝑇 → ( bday ‘ 𝑐 ) = ( bday ‘ 𝑇 ) )
25	24	sseq1d	⊢ ( 𝑐 = 𝑇 → ( ( bday ‘ 𝑐 ) ⊆ 𝑂 ↔ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) )
26	21 23 25	3anbi123d	⊢ ( 𝑐 = 𝑇 → ( ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ∧ ( bday ‘ 𝑐 ) ⊆ 𝑂 ) ↔ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) )
27	26	rspcev	⊢ ( ( 𝑇 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) → ∃ 𝑐 ∈ No ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ∧ ( bday ‘ 𝑐 ) ⊆ 𝑂 ) )
28	19 27	jaoi	⊢ ( ( ( 𝑆 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑆 ∧ ∀ 𝑏 ∈ 𝐵 𝑆 <s 𝑏 ∧ ( bday ‘ 𝑆 ) ⊆ 𝑂 ) ) ∨ ( 𝑇 ∈ No ∧ ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑇 ∧ ∀ 𝑏 ∈ 𝐵 𝑇 <s 𝑏 ∧ ( bday ‘ 𝑇 ) ⊆ 𝑂 ) ) ) → ∃ 𝑐 ∈ No ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ∧ ( bday ‘ 𝑐 ) ⊆ 𝑂 ) )
29	11 28	syl	⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ∃ 𝑐 ∈ No ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ∧ ( bday ‘ 𝑐 ) ⊆ 𝑂 ) )
30	8 29	sylan	⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ∧ ( 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ) → ∃ 𝑐 ∈ No ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 𝑐 <s 𝑏 ∧ ( bday ‘ 𝑐 ) ⊆ 𝑂 ) )