Theorem weiunval 37441

Description: Value of the relation constructed in weiunpo 37444, weiunso 37445, weiunfr 37446, and weiunse 37447. (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 6915	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑦) = (𝐹‘𝐶))
3		simpr 490	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → 𝑧 = 𝐷)
4	3	fveq2d 6915	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑧) = (𝐹‘𝐷))
5	2, 4	breq12d 5119	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ↔ (𝐹‘𝐶)𝑅(𝐹‘𝐷)))
6	2, 4	eqeq12d 2779	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝐹‘𝐶) = (𝐹‘𝐷)))
7	2	csbeq1d 3855	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝐶) / 𝑥⦌𝑆)
8	1, 7, 3	breq123d 5120	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧 ↔ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))
9	6, 8	anbi12d 644	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧) ↔ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷)))
10	5, 9	orbi12d 932	. 2 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)) ↔ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
11		weiun.2	. 2 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
12	10, 11	brab2a 5750	1 ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2147  ∀wral 3080  {crab 3416  ⦋csb 3851  ∪ ciun 4954   class class class wbr 5106  {copab 5171   ↦ cmpt 5190  ‘cfv 6561  ℩crio 7402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-xp 5662  df-iota 6515  df-fv 6569

This theorem is used by:  weiunpo  37444  weiunso  37445  weiunfr  37446  weiunse  37447