Metamath Proof Explorer

Theorem weiunwe

Description: A well-ordering on an indexed union can be constructed from a well-ordering on its index class and a collection of well-orderings on its members. (Contributed by Matthew House, 23-Aug-2025)

Ref Expression
Hypotheses weiun.1 ⊢ F = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
weiun.2 ⊢ T = y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ F ⁡ y R F ⁡ z ∨ F ⁡ y = F ⁡ z ∧ y ⦋ F ⁡ y / x⦌ S z
Assertion weiunwe ⊢ R We A ∧ R Se A ∧ ∀ x ∈ A S We B → T We ⋃ x ∈ A B

Proof

Step Hyp Ref Expression
1 weiun.1 ⊢ F = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
2 weiun.2 ⊢ T = y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ F ⁡ y R F ⁡ z ∨ F ⁡ y = F ⁡ z ∧ y ⦋ F ⁡ y / x⦌ S z
3 wefr ⊢ S We B → S Fr B
4 3 ralimi ⊢ ∀ x ∈ A S We B → ∀ x ∈ A S Fr B
5 1 2 weiunfr ⊢ R We A ∧ R Se A ∧ ∀ x ∈ A S Fr B → T Fr ⋃ x ∈ A B
6 4 5 syl3an3 ⊢ R We A ∧ R Se A ∧ ∀ x ∈ A S We B → T Fr ⋃ x ∈ A B
7 weso ⊢ S We B → S Or B
8 7 ralimi ⊢ ∀ x ∈ A S We B → ∀ x ∈ A S Or B
9 1 2 weiunso ⊢ R We A ∧ R Se A ∧ ∀ x ∈ A S Or B → T Or ⋃ x ∈ A B
10 8 9 syl3an3 ⊢ R We A ∧ R Se A ∧ ∀ x ∈ A S We B → T Or ⋃ x ∈ A B
11 df-we ⊢ T We ⋃ x ∈ A B ↔ T Fr ⋃ x ∈ A B ∧ T Or ⋃ x ∈ A B
12 6 10 11 sylanbrc ⊢ R We A ∧ R Se A ∧ ∀ x ∈ A S We B → T We ⋃ x ∈ A B