Theorem weiunfrlem1 36380

Description: Lemma for weiunfr 36382. (Contributed by Matthew House, 23-Aug-2025.)

Hypotheses

Ref	Expression
weiunfrlem1.1	⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
weiunfrlem1.2	⊢ 𝐶 = (℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)

Assertion

Ref	Expression
weiunfrlem1	⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐶 ∈ (𝐹 “ 𝑟) ∧ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶))

Distinct variable groups:   𝑥,𝑠   𝑠,𝑟,𝑡,𝑤   𝐴,𝑠,𝑡,𝑤   𝑢,𝐴,𝑣,𝑥,𝑤   𝐵,𝑠   𝑢,𝐵,𝑣,𝑤   𝑤,𝐶   𝑢,𝑅,𝑣   𝑅,𝑠,𝑡,𝑤   𝐹,𝑠,𝑡,𝑤

Allowed substitution hints:   𝐴(𝑟)   𝐵(𝑥,𝑡,𝑟)   𝐶(𝑥,𝑣,𝑢,𝑡,𝑠,𝑟)   𝑅(𝑥,𝑟)   𝐹(𝑥,𝑣,𝑢,𝑟)

Proof of Theorem weiunfrlem1

Step	Hyp	Ref	Expression
1		weiunfrlem1.2	. . . 4 ⊢ 𝐶 = (℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)
2		simpl 482	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑅 We 𝐴 ∧ 𝑅 Se 𝐴))
3		weiunfrlem1.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
4	3	weiunlem1 36376	. . . . . . . . 9 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))
5	4	adantr 480	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))
6	5	simp1d 1142	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴)
7	6	fimassd 6767	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹 “ 𝑟) ⊆ 𝐴)
8		simprl 770	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
9	6	fdmd 6756	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → dom 𝐹 = ∪ 𝑥 ∈ 𝐴 𝐵)
10	8, 9	sseqtrrd 4044	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ⊆ dom 𝐹)
11		sseqin2 4238	. . . . . . . . 9 ⊢ (𝑟 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑟) = 𝑟)
12	10, 11	sylib 218	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (dom 𝐹 ∩ 𝑟) = 𝑟)
13		simprr 772	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ≠ ∅)
14	12, 13	eqnetrd 3010	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (dom 𝐹 ∩ 𝑟) ≠ ∅)
15	14	imadisjlnd 6109	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹 “ 𝑟) ≠ ∅)
16		wereu2 5696	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ ((𝐹 “ 𝑟) ⊆ 𝐴 ∧ (𝐹 “ 𝑟) ≠ ∅)) → ∃!𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)
17	2, 7, 15, 16	syl12anc 836	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃!𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)
18		riotacl2 7418	. . . . 5 ⊢ (∃!𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠 → (℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠) ∈ {𝑠 ∈ (𝐹 “ 𝑟) ∣ ∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠})
19	17, 18	syl 17	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠) ∈ {𝑠 ∈ (𝐹 “ 𝑟) ∣ ∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠})
20	1, 19	eqeltrid 2842	. . 3 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐶 ∈ {𝑠 ∈ (𝐹 “ 𝑟) ∣ ∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠})
21	6	ffnd 6747	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐹 Fn ∪ 𝑥 ∈ 𝐴 𝐵)
22		breq1 5172	. . . . . . 7 ⊢ (𝑡 = (𝐹‘𝑤) → (𝑡𝑅𝑠 ↔ (𝐹‘𝑤)𝑅𝑠))
23	22	notbid 318	. . . . . 6 ⊢ (𝑡 = (𝐹‘𝑤) → (¬ 𝑡𝑅𝑠 ↔ ¬ (𝐹‘𝑤)𝑅𝑠))
24	23	ralima 7272	. . . . 5 ⊢ ((𝐹 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) → (∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠 ↔ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝑠))
25	24	rabbidv 3446	. . . 4 ⊢ ((𝐹 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) → {𝑠 ∈ (𝐹 “ 𝑟) ∣ ∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠} = {𝑠 ∈ (𝐹 “ 𝑟) ∣ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝑠})
26	21, 8, 25	syl2anc 583	. . 3 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → {𝑠 ∈ (𝐹 “ 𝑟) ∣ ∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠} = {𝑠 ∈ (𝐹 “ 𝑟) ∣ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝑠})
27	20, 26	eleqtrd 2840	. 2 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐶 ∈ {𝑠 ∈ (𝐹 “ 𝑟) ∣ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝑠})
28		nfriota1 7408	. . . 4 ⊢ Ⅎ𝑠(℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)
29	1, 28	nfcxfr 2902	. . 3 ⊢ Ⅎ𝑠𝐶
30		nfcv 2904	. . 3 ⊢ Ⅎ𝑠(𝐹 “ 𝑟)
31		nfcv 2904	. . . 4 ⊢ Ⅎ𝑠𝑟
32		nfcv 2904	. . . . . 6 ⊢ Ⅎ𝑠(𝐹‘𝑤)
33		nfcv 2904	. . . . . 6 ⊢ Ⅎ𝑠𝑅
34	32, 33, 29	nfbr 5216	. . . . 5 ⊢ Ⅎ𝑠(𝐹‘𝑤)𝑅𝐶
35	34	nfn 1856	. . . 4 ⊢ Ⅎ𝑠 ¬ (𝐹‘𝑤)𝑅𝐶
36	31, 35	nfralw 3312	. . 3 ⊢ Ⅎ𝑠∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶
37		breq2 5173	. . . . 5 ⊢ (𝑠 = 𝐶 → ((𝐹‘𝑤)𝑅𝑠 ↔ (𝐹‘𝑤)𝑅𝐶))
38	37	notbid 318	. . . 4 ⊢ (𝑠 = 𝐶 → (¬ (𝐹‘𝑤)𝑅𝑠 ↔ ¬ (𝐹‘𝑤)𝑅𝐶))
39	38	ralbidv 3180	. . 3 ⊢ (𝑠 = 𝐶 → (∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝑠 ↔ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶))
40	29, 30, 36, 39	elrabf 3699	. 2 ⊢ (𝐶 ∈ {𝑠 ∈ (𝐹 “ 𝑟) ∣ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝑠} ↔ (𝐶 ∈ (𝐹 “ 𝑟) ∧ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶))
41	27, 40	sylib 218	1 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐶 ∈ (𝐹 “ 𝑟) ∧ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2103   ≠ wne 2942  ∀wral 3063  ∃!wreu 3381  {crab 3438  ⦋csb 3915   ∩ cin 3969   ⊆ wss 3970  ∅c0 4347  ∪ ciun 5019   class class class wbr 5169   ↦ cmpt 5252   Se wse 5652   We wwe 5653  dom cdm 5699   “ cima 5702   Fn wfn 6567  ⟶wf 6568  ‘cfv 6572  ℩crio 7400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pr 5450

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-id 5597  df-po 5611  df-so 5612  df-fr 5654  df-se 5655  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-fv 6580  df-riota 7401

This theorem is referenced by:  weiunfrlem2  36381