Metamath Proof Explorer


Theorem weiunlem1

Description: Lemma for weiunpo , weiunso , weiunfr , and weiunse . (Contributed by Matthew House, 8-Sep-2025)

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

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 ( 𝐶 𝑇 𝐷 ↔ ( ( 𝐶 𝑥𝐴 𝐵𝐷 𝑥𝐴 𝐵 ) ∧ ( ( 𝐹𝐶 ) 𝑅 ( 𝐹𝐷 ) ∨ ( ( 𝐹𝐶 ) = ( 𝐹𝐷 ) ∧ 𝐶 ( 𝐹𝐶 ) / 𝑥 𝑆 𝐷 ) ) ) )