Theorem weiunval 36954

Description: Value of the relation constructed in weiunpo 36957, weiunso 36958, weiunfr 36959, and weiunse 36960. (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 487	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → 𝑦 = 𝐶)
2	1	fveq2d 6887	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑦) = (𝐹‘𝐶))
3		simpr 489	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → 𝑧 = 𝐷)
4	3	fveq2d 6887	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑧) = (𝐹‘𝐷))
5	2, 4	breq12d 5123	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ↔ (𝐹‘𝐶)𝑅(𝐹‘𝐷)))
6	2, 4	eqeq12d 2779	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝐹‘𝐶) = (𝐹‘𝐷)))
7	2	csbeq1d 3858	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝐶) / 𝑥⦌𝑆)
8	1, 7, 3	breq123d 5124	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧 ↔ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))
9	6, 8	anbi12d 643	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧) ↔ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷)))
10	5, 9	orbi12d 931	. 2 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)) ↔ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
11		weiun.2	. 2 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
12	10, 11	brab2a 5756	1 ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143  ∀wral 3079  {crab 3416  ⦋csb 3854  ∪ ciun 4957   class class class wbr 5110  {copab 5174   ↦ cmpt 5193  ‘cfv 6538  ℩crio 7368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-iota 6494  df-fv 6546

This theorem is referenced by:  weiunpo  36957  weiunso  36958  weiunfr  36959  weiunse  36960