Theorem weiunval 36697

Description: Value of the relation constructed in weiunpo 36700, weiunso 36701, weiunfr 36702, and weiunse 36703. (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 483	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → 𝑦 = 𝐶)
2	1	fveq2d 6838	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑦) = (𝐹‘𝐶))
3		simpr 485	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → 𝑧 = 𝐷)
4	3	fveq2d 6838	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝐹‘𝑧) = (𝐹‘𝐷))
5	2, 4	breq12d 5092	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ↔ (𝐹‘𝐶)𝑅(𝐹‘𝐷)))
6	2, 4	eqeq12d 2756	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝐹‘𝐶) = (𝐹‘𝐷)))
7	2	csbeq1d 3842	. . . . 5 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝐶) / 𝑥⦌𝑆)
8	1, 7, 3	breq123d 5093	. . . 4 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧 ↔ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))
9	6, 8	anbi12d 638	. . 3 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧) ↔ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷)))
10	5, 9	orbi12d 924	. 2 ⊢ ((𝑦 = 𝐶 ∧ 𝑧 = 𝐷) → (((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)) ↔ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
11		weiun.2	. 2 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
12	10, 11	brab2a 5718	1 ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396   ∨ wo 853   = wceq 1547   ∈ wcel 2119  ∀wral 3054  {crab 3392  ⦋csb 3838  ∪ ciun 4928   class class class wbr 5079  {copab 5141   ↦ cmpt 5160  ‘cfv 6492  ℩crio 7319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-iota 6448  df-fv 6500

This theorem is referenced by:  weiunpo  36700  weiunso  36701  weiunfr  36702  weiunse  36703