Theorem weiunval

Description: Value of the relation constructed in weiunpo , weiunso , weiunfr , and weiunse . (Contributed by Matthew House, 8-Sep-2025)

	Ref	Expression
Hypotheses	weiun.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
	weiun.2	⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
Assertion	weiunval	⊢ ( 𝐶 𝑇 𝐷 ↔ ( ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝐶 ) 𝑅 ( 𝐹 ‘ 𝐷 ) ∨ ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ∧ 𝐶 ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		weiun.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2		weiun.2	⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
3		simpl	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → 𝑦 = 𝐶 )
4	3	fveq2d	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐶 ) )
5		simpr	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → 𝑧 = 𝐷 )
6	5	fveq2d	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐷 ) )
7	4 6	breq12d	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝐶 ) 𝑅 ( 𝐹 ‘ 𝐷 ) ) )
8	4 6	eqeq12d	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ) )
9	4	csbeq1d	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 )
10	3 9 5	breq123d	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝐶 ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 𝐷 ) )
11	8 10	anbi12d	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ∧ 𝐶 ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 𝐷 ) ) )
12	7 11	orbi12d	⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝐶 ) 𝑅 ( 𝐹 ‘ 𝐷 ) ∨ ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ∧ 𝐶 ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 𝐷 ) ) ) )
13	12 2	brab2a	⊢ ( 𝐶 𝑇 𝐷 ↔ ( ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝐶 ) 𝑅 ( 𝐹 ‘ 𝐷 ) ∨ ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ∧ 𝐶 ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 𝐷 ) ) ) )