Metamath Proof Explorer

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 ⊢ S = if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
noetalem2.2 ⊢ T = if ∃ x ∈ B ∀ y ∈ B ¬ y < s x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 g ∈ y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
Assertion noetalem2 ⊢ A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ W ∧ ∀ a ∈ A ∀ b ∈ B a < s b ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ c ∈ No ∀ a ∈ A a < s c ∧ ∀ b ∈ B c < s b ∧ bday ⁡ c ⊆ O

Proof

Step Hyp Ref Expression
1 noetalem2.1 ⊢ S = if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
2 noetalem2.2 ⊢ T = if ∃ x ∈ B ∀ y ∈ B ¬ y < s x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 g ∈ y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
3 elex ⊢ A ∈ V → A ∈ V
4 3 anim2i ⊢ A ⊆ No ∧ A ∈ V → A ⊆ No ∧ A ∈ V
5 elex ⊢ B ∈ W → B ∈ V
6 5 anim2i ⊢ B ⊆ No ∧ B ∈ W → B ⊆ No ∧ B ∈ V
7 id ⊢ ∀ a ∈ A ∀ b ∈ B a < s b → ∀ a ∈ A ∀ b ∈ B a < s b
8 4 6 7 3anim123i ⊢ A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ W ∧ ∀ a ∈ A ∀ b ∈ B a < s b → A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ V ∧ ∀ a ∈ A ∀ b ∈ B a < s b
9 eqid ⊢ S ∪ suc ⁡ ⋃ bday B ∖ dom ⁡ S × 1 𝑜 = S ∪ suc ⁡ ⋃ bday B ∖ dom ⁡ S × 1 𝑜
10 eqid ⊢ T ∪ suc ⁡ ⋃ bday A ∖ dom ⁡ T × 2 𝑜 = T ∪ suc ⁡ ⋃ bday A ∖ dom ⁡ T × 2 𝑜
11 1 2 9 10 noetalem1 ⊢ A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ V ∧ ∀ a ∈ A ∀ b ∈ B a < s b ∧ O ∈ On ∧ bday A ∪ B ⊆ O → S ∈ No ∧ ∀ a ∈ A a < s S ∧ ∀ b ∈ B S < s b ∧ bday ⁡ S ⊆ O ∨ T ∈ No ∧ ∀ a ∈ A a < s T ∧ ∀ b ∈ B T < s b ∧ bday ⁡ T ⊆ O
12 breq2 ⊢ c = S → a < s c ↔ a < s S
13 12 ralbidv ⊢ c = S → ∀ a ∈ A a < s c ↔ ∀ a ∈ A a < s S
14 breq1 ⊢ c = S → c < s b ↔ S < s b
15 14 ralbidv ⊢ c = S → ∀ b ∈ B c < s b ↔ ∀ b ∈ B S < s b
16 fveq2 ⊢ c = S → bday ⁡ c = bday ⁡ S
17 16 sseq1d ⊢ c = S → bday ⁡ c ⊆ O ↔ bday ⁡ S ⊆ O
18 13 15 17 3anbi123d ⊢ c = S → ∀ a ∈ A a < s c ∧ ∀ b ∈ B c < s b ∧ bday ⁡ c ⊆ O ↔ ∀ a ∈ A a < s S ∧ ∀ b ∈ B S < s b ∧ bday ⁡ S ⊆ O
19 18 rspcev ⊢ S ∈ No ∧ ∀ a ∈ A a < s S ∧ ∀ b ∈ B S < s b ∧ bday ⁡ S ⊆ O → ∃ c ∈ No ∀ a ∈ A a < s c ∧ ∀ b ∈ B c < s b ∧ bday ⁡ c ⊆ O
20 breq2 ⊢ c = T → a < s c ↔ a < s T
21 20 ralbidv ⊢ c = T → ∀ a ∈ A a < s c ↔ ∀ a ∈ A a < s T
22 breq1 ⊢ c = T → c < s b ↔ T < s b
23 22 ralbidv ⊢ c = T → ∀ b ∈ B c < s b ↔ ∀ b ∈ B T < s b
24 fveq2 ⊢ c = T → bday ⁡ c = bday ⁡ T
25 24 sseq1d ⊢ c = T → bday ⁡ c ⊆ O ↔ bday ⁡ T ⊆ O
26 21 23 25 3anbi123d ⊢ c = T → ∀ a ∈ A a < s c ∧ ∀ b ∈ B c < s b ∧ bday ⁡ c ⊆ O ↔ ∀ a ∈ A a < s T ∧ ∀ b ∈ B T < s b ∧ bday ⁡ T ⊆ O
27 26 rspcev ⊢ T ∈ No ∧ ∀ a ∈ A a < s T ∧ ∀ b ∈ B T < s b ∧ bday ⁡ T ⊆ O → ∃ c ∈ No ∀ a ∈ A a < s c ∧ ∀ b ∈ B c < s b ∧ bday ⁡ c ⊆ O
28 19 27 jaoi ⊢ S ∈ No ∧ ∀ a ∈ A a < s S ∧ ∀ b ∈ B S < s b ∧ bday ⁡ S ⊆ O ∨ T ∈ No ∧ ∀ a ∈ A a < s T ∧ ∀ b ∈ B T < s b ∧ bday ⁡ T ⊆ O → ∃ c ∈ No ∀ a ∈ A a < s c ∧ ∀ b ∈ B c < s b ∧ bday ⁡ c ⊆ O
29 11 28 syl ⊢ A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ V ∧ ∀ a ∈ A ∀ b ∈ B a < s b ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ c ∈ No ∀ a ∈ A a < s c ∧ ∀ b ∈ B c < s b ∧ bday ⁡ c ⊆ O
30 8 29 sylan ⊢ A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ W ∧ ∀ a ∈ A ∀ b ∈ B a < s b ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ c ∈ No ∀ a ∈ A a < s c ∧ ∀ b ∈ B c < s b ∧ bday ⁡ c ⊆ O