Metamath Proof Explorer

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 ⊢ 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 weiunval ⊢ C T D ↔ C ∈ ⋃ x ∈ A B ∧ D ∈ ⋃ x ∈ A B ∧ F ⁡ C R F ⁡ D ∨ F ⁡ C = F ⁡ D ∧ C ⦋ F ⁡ C / x⦌ S D

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 simpl ⊢ y = C ∧ z = D → y = C
4 3 fveq2d ⊢ y = C ∧ z = D → F ⁡ y = F ⁡ C
5 simpr ⊢ y = C ∧ z = D → z = D
6 5 fveq2d ⊢ y = C ∧ z = D → F ⁡ z = F ⁡ D
7 4 6 breq12d ⊢ y = C ∧ z = D → F ⁡ y R F ⁡ z ↔ F ⁡ C R F ⁡ D
8 4 6 eqeq12d ⊢ y = C ∧ z = D → F ⁡ y = F ⁡ z ↔ F ⁡ C = F ⁡ D
9 4 csbeq1d ⊢ y = C ∧ z = D → ⦋ F ⁡ y / x⦌ S = ⦋ F ⁡ C / x⦌ S
10 3 9 5 breq123d ⊢ y = C ∧ z = D → y ⦋ F ⁡ y / x⦌ S z ↔ C ⦋ F ⁡ C / x⦌ S D
11 8 10 anbi12d ⊢ y = C ∧ z = D → F ⁡ y = F ⁡ z ∧ y ⦋ F ⁡ y / x⦌ S z ↔ F ⁡ C = F ⁡ D ∧ C ⦋ F ⁡ C / x⦌ S D
12 7 11 orbi12d ⊢ y = C ∧ z = D → F ⁡ y R F ⁡ z ∨ F ⁡ y = F ⁡ z ∧ y ⦋ F ⁡ y / x⦌ S z ↔ F ⁡ C R F ⁡ D ∨ F ⁡ C = F ⁡ D ∧ C ⦋ F ⁡ C / x⦌ S D
13 12 2 brab2a ⊢ C T D ↔ C ∈ ⋃ x ∈ A B ∧ D ∈ ⋃ x ∈ A B ∧ F ⁡ C R F ⁡ D ∨ F ⁡ C = F ⁡ D ∧ C ⦋ F ⁡ C / x⦌ S D