Theorem weiunlem2

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

	Ref	Expression
Hypothesis	weiunlem2.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
Assertion	weiunlem2	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑠 ∈ 𝐴 ( 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 → ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ) ) )

Proof

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