Theorem weiunval 36675

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

Hypotheses

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

Assertion

Ref	Expression
weiunval	⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))

Distinct variable groups:   𝑢,𝐴,𝑣,𝑤,𝑥   𝑦,𝐴,𝑧,𝑥   𝑢,𝐵,𝑣,𝑤   𝑦,𝐵,𝑧   𝑦,𝐶,𝑧   𝑦,𝐷,𝑧   𝑦,𝐹,𝑧   𝑢,𝑅,𝑣,𝑤   𝑦,𝑅,𝑧   𝑦,𝑆,𝑧

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥,𝑤,𝑣,𝑢)   𝐷(𝑥,𝑤,𝑣,𝑢)   𝑅(𝑥)   𝑆(𝑥,𝑤,𝑣,𝑢)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝐹(𝑥,𝑤,𝑣,𝑢)

Proof of Theorem weiunval

Step	Hyp	Ref	Expression
1		simpl 482	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → 𝑦 = 𝐶)
2	1	fveq2d 6846	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑦) = (𝐹‘𝐶))
3		simpr 484	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → 𝑧 = 𝐷)
4	3	fveq2d 6846	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑧) = (𝐹‘𝐷))
5	2, 4	breq12d 5113	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ↔ (𝐹‘𝐶)𝑅(𝐹‘𝐷)))
6	2, 4	eqeq12d 2753	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝐹‘𝐶) = (𝐹‘𝐷)))
7	2	csbeq1d 3855	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝐶) / 𝑥⦌𝑆)
8	1, 7, 3	breq123d 5114	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧 ↔ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))
9	6, 8	anbi12d 633	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧) ↔ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷)))
10	5, 9	orbi12d 919	. 2 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)) ↔ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
11		weiun.2	. 2 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
12	10, 11	brab2a 5725	1 ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {crab 3401  ⦋csb 3851  ∪ ciun 4948   class class class wbr 5100  {copab 5162   ↦ cmpt 5181  ‘cfv 6500  ℩crio 7324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-iota 6456  df-fv 6508

This theorem is referenced by:  weiunpo  36678  weiunso  36679  weiunfr  36680  weiunse  36681