Theorem weiunlem2 36377

Description: Lemma for weiunpo 36378, weiunso 36379, and weiunse 36383. (Contributed by Matthew House, 23-Aug-2025.)

Hypothesis

Ref	Expression
weiunlem2.1	⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))

Assertion

Ref	Expression
weiunlem2	⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑠 ∈ 𝐴 (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡))))

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

Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥)   𝐹(𝑥,𝑤,𝑣,𝑢)

Proof of Theorem weiunlem2

Step	Hyp	Ref	Expression
1		weiunlem2.1	. . 3 ⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
2	1	weiunlem1 36376	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))
3		biid 261	. . 3 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴)
4		nfv 1913	. . . 4 ⊢ Ⅎ𝑡 𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵
5		nfmpt1 5277	. . . . . . . 8 ⊢ Ⅎ𝑤(𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
6	1, 5	nfcxfr 2902	. . . . . . 7 ⊢ Ⅎ𝑤𝐹
7		nfcv 2904	. . . . . . 7 ⊢ Ⅎ𝑤𝑡
8	6, 7	nffv 6929	. . . . . 6 ⊢ Ⅎ𝑤(𝐹‘𝑡)
9		nfcv 2904	. . . . . 6 ⊢ Ⅎ𝑤𝐵
10	8, 9	nfcsbw 3942	. . . . 5 ⊢ Ⅎ𝑤⦋(𝐹‘𝑡) / 𝑥⦌𝐵
11	10	nfcri 2895	. . . 4 ⊢ Ⅎ𝑤 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵
12		id 22	. . . . 5 ⊢ (𝑤 = 𝑡 → 𝑤 = 𝑡)
13		fveq2 6919	. . . . . 6 ⊢ (𝑤 = 𝑡 → (𝐹‘𝑤) = (𝐹‘𝑡))
14	13	csbeq1d 3919	. . . . 5 ⊢ (𝑤 = 𝑡 → ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
15	12, 14	eleq12d 2832	. . . 4 ⊢ (𝑤 = 𝑡 → (𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ↔ 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵))
16	4, 11, 15	cbvralw 3307	. . 3 ⊢ (∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ↔ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
17		nfv 1913	. . . 4 ⊢ Ⅎ𝑡∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))
18		nfcv 2904	. . . . 5 ⊢ Ⅎ𝑤𝐴
19		nfv 1913	. . . . . 6 ⊢ Ⅎ𝑤 𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵
20		nfcv 2904	. . . . . . . 8 ⊢ Ⅎ𝑤𝑠
21		nfcv 2904	. . . . . . . 8 ⊢ Ⅎ𝑤𝑅
22	20, 21, 8	nfbr 5216	. . . . . . 7 ⊢ Ⅎ𝑤 𝑠𝑅(𝐹‘𝑡)
23	22	nfn 1856	. . . . . 6 ⊢ Ⅎ𝑤 ¬ 𝑠𝑅(𝐹‘𝑡)
24	19, 23	nfim 1895	. . . . 5 ⊢ Ⅎ𝑤(𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡))
25	18, 24	nfralw 3312	. . . 4 ⊢ Ⅎ𝑤∀𝑠 ∈ 𝐴 (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡))
26		nfv 1913	. . . . . 6 ⊢ Ⅎ𝑠(𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))
27		nfv 1913	. . . . . . 7 ⊢ Ⅎ𝑣 𝑤 ∈ ⦋𝑠 / 𝑥⦌𝐵
28		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑣𝑠
29		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑣𝑅
30		nfcv 2904	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣∪ 𝑥 ∈ 𝐴 𝐵
31		nfra1 3285	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢
32		nfcv 2904	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣{𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}
33	31, 32	nfriota 7414	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣(℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)
34	30, 33	nfmpt 5276	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
35	1, 34	nfcxfr 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑣𝐹
36		nfcv 2904	. . . . . . . . . 10 ⊢ Ⅎ𝑣𝑤
37	35, 36	nffv 6929	. . . . . . . . 9 ⊢ Ⅎ𝑣(𝐹‘𝑤)
38	28, 29, 37	nfbr 5216	. . . . . . . 8 ⊢ Ⅎ𝑣 𝑠𝑅(𝐹‘𝑤)
39	38	nfn 1856	. . . . . . 7 ⊢ Ⅎ𝑣 ¬ 𝑠𝑅(𝐹‘𝑤)
40	27, 39	nfim 1895	. . . . . 6 ⊢ Ⅎ𝑣(𝑤 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑤))
41		csbeq1 3918	. . . . . . . 8 ⊢ (𝑣 = 𝑠 → ⦋𝑣 / 𝑥⦌𝐵 = ⦋𝑠 / 𝑥⦌𝐵)
42	41	eleq2d 2824	. . . . . . 7 ⊢ (𝑣 = 𝑠 → (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 ↔ 𝑤 ∈ ⦋𝑠 / 𝑥⦌𝐵))
43		breq1 5172	. . . . . . . 8 ⊢ (𝑣 = 𝑠 → (𝑣𝑅(𝐹‘𝑤) ↔ 𝑠𝑅(𝐹‘𝑤)))
44	43	notbid 318	. . . . . . 7 ⊢ (𝑣 = 𝑠 → (¬ 𝑣𝑅(𝐹‘𝑤) ↔ ¬ 𝑠𝑅(𝐹‘𝑤)))
45	42, 44	imbi12d 344	. . . . . 6 ⊢ (𝑣 = 𝑠 → ((𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)) ↔ (𝑤 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑤))))
46	26, 40, 45	cbvralw 3307	. . . . 5 ⊢ (∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)) ↔ ∀𝑠 ∈ 𝐴 (𝑤 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑤)))
47		eleq1w 2821	. . . . . . 7 ⊢ (𝑤 = 𝑡 → (𝑤 ∈ ⦋𝑠 / 𝑥⦌𝐵 ↔ 𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵))
48	13	breq2d 5181	. . . . . . . 8 ⊢ (𝑤 = 𝑡 → (𝑠𝑅(𝐹‘𝑤) ↔ 𝑠𝑅(𝐹‘𝑡)))
49	48	notbid 318	. . . . . . 7 ⊢ (𝑤 = 𝑡 → (¬ 𝑠𝑅(𝐹‘𝑤) ↔ ¬ 𝑠𝑅(𝐹‘𝑡)))
50	47, 49	imbi12d 344	. . . . . 6 ⊢ (𝑤 = 𝑡 → ((𝑤 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑤)) ↔ (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡))))
51	50	ralbidv 3180	. . . . 5 ⊢ (𝑤 = 𝑡 → (∀𝑠 ∈ 𝐴 (𝑤 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑤)) ↔ ∀𝑠 ∈ 𝐴 (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡))))
52	46, 51	bitrid 283	. . . 4 ⊢ (𝑤 = 𝑡 → (∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)) ↔ ∀𝑠 ∈ 𝐴 (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡))))
53	17, 25, 52	cbvralw 3307	. . 3 ⊢ (∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)) ↔ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑠 ∈ 𝐴 (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡)))
54	3, 16, 53	3anbi123i 1155	. 2 ⊢ ((𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))) ↔ (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑠 ∈ 𝐴 (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡))))
55	2, 54	sylib 218	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑠 ∈ 𝐴 (𝑡 ∈ ⦋𝑠 / 𝑥⦌𝐵 → ¬ 𝑠𝑅(𝐹‘𝑡))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2103  ∀wral 3063  {crab 3438  ⦋csb 3915  ∪ ciun 5019   class class class wbr 5169   ↦ cmpt 5252   Se wse 5652   We wwe 5653  ⟶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:  weiunpo  36378  weiunso  36379  weiunse  36383