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	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
	weiun.2	⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
Assertion	weiunwe	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 ) → 𝑇 We ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		weiun.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2		weiun.2	⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
3		wefr	⊢ ( 𝑆 We 𝐵 → 𝑆 Fr 𝐵 )
4	3	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 → ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 )
5	1 2	weiunfr	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 )
6	4 5	syl3an3	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 ) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 )
7		weso	⊢ ( 𝑆 We 𝐵 → 𝑆 Or 𝐵 )
8	7	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 → ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 )
9	1 2	weiunso	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) → 𝑇 Or ∪ 𝑥 ∈ 𝐴 𝐵 )
10	8 9	syl3an3	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 ) → 𝑇 Or ∪ 𝑥 ∈ 𝐴 𝐵 )
11		df-we	⊢ ( 𝑇 We ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑇 Or ∪ 𝑥 ∈ 𝐴 𝐵 ) )
12	6 10 11	sylanbrc	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 We 𝐵 ) → 𝑇 We ∪ 𝑥 ∈ 𝐴 𝐵 )