Theorem weiunval 37342

Description: Value of the relation constructed in weiunpo 37345, weiunso 37346, weiunfr 37347, and weiunse 37348. (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 488	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → 𝑦 = 𝐶)
2	1	fveq2d 6889	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑦) = (𝐹‘𝐶))
3		simpr 490	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → 𝑧 = 𝐷)
4	3	fveq2d 6889	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑧) = (𝐹‘𝐷))
5	2, 4	breq12d 5115	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ↔ (𝐹‘𝐶)𝑅(𝐹‘𝐷)))
6	2, 4	eqeq12d 2776	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝐹‘𝐶) = (𝐹‘𝐷)))
7	2	csbeq1d 3850	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝐶) / 𝑥⦌𝑆)
8	1, 7, 3	breq123d 5116	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧 ↔ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))
9	6, 8	anbi12d 644	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧) ↔ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷)))
10	5, 9	orbi12d 932	. 2 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)) ↔ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
11		weiun.2	. 2 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
12	10, 11	brab2a 5743	1 ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1569   ∈ wcel 2144  ∀wral 3076  {crab 3412  ⦋csb 3846  ∪ ciun 4950   class class class wbr 5102  {copab 5166   ↦ cmpt 5185  ‘cfv 6538  ℩crio 7376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-iota 6494  df-fv 6546

This theorem is used by:  weiunpo  37345  weiunso  37346  weiunfr  37347  weiunse  37348