Theorem weiunlem1

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

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

Proof

Step	Hyp	Ref	Expression
1		weiunlem1.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ⊆ 𝐴
3		eliun	⊢ ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
4		rabn0	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
5	3 4	sylbb2	⊢ ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ≠ ∅ )
6		wereu2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ≠ ∅ ) ) → ∃! 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 )
7	2 6	mpanr1	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ≠ ∅ ) → ∃! 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 )
8	5 7	sylan2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∃! 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 )
9		riotacl	⊢ ( ∃! 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 → ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } )
10	8 9	syl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } )
11	2 10	sselid	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) ∈ 𝐴 )
12	11 1	fmptd	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
13		simpr	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
14	1	fvmpt2	⊢ ( ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ) → ( 𝐹 ‘ 𝑤 ) = ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
15	13 10 14	syl2anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝐹 ‘ 𝑤 ) = ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
16	15 10	eqeltrd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝐹 ‘ 𝑤 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } )
17		nfcv	⊢ Ⅎ 𝑥 𝐴
18	17	elrabsf	⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ↔ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐴 ∧ [ ( 𝐹 ‘ 𝑤 ) / 𝑥 ] 𝑤 ∈ 𝐵 ) )
19	16 18	sylib	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐴 ∧ [ ( 𝐹 ‘ 𝑤 ) / 𝑥 ] 𝑤 ∈ 𝐵 ) )
20	19	simprd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → [ ( 𝐹 ‘ 𝑤 ) / 𝑥 ] 𝑤 ∈ 𝐵 )
21		sbcel2	⊢ ( [ ( 𝐹 ‘ 𝑤 ) / 𝑥 ] 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 )
22	20 21	sylib	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 )
23	22	ralrimiva	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 )
24	15	eqcomd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) = ( 𝐹 ‘ 𝑤 ) )
25		nfcv	⊢ Ⅎ 𝑢 ∪ 𝑥 ∈ 𝐴 𝐵
26		nfriota1	⊢ Ⅎ 𝑢 ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 )
27	25 26	nfmpt	⊢ Ⅎ 𝑢 ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
28	1 27	nfcxfr	⊢ Ⅎ 𝑢 𝐹
29		nfcv	⊢ Ⅎ 𝑢 𝑤
30	28 29	nffv	⊢ Ⅎ 𝑢 ( 𝐹 ‘ 𝑤 )
31		nfcv	⊢ Ⅎ 𝑢 { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 }
32		nfcv	⊢ Ⅎ 𝑢 𝑣
33		nfcv	⊢ Ⅎ 𝑢 𝑅
34	32 33 30	nfbr	⊢ Ⅎ 𝑢 𝑣 𝑅 ( 𝐹 ‘ 𝑤 )
35	34	nfn	⊢ Ⅎ 𝑢 ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 )
36	31 35	nfralw	⊢ Ⅎ 𝑢 ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 )
37		nfcv	⊢ Ⅎ 𝑣 ∪ 𝑥 ∈ 𝐴 𝐵
38		nfra1	⊢ Ⅎ 𝑣 ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢
39		nfcv	⊢ Ⅎ 𝑣 { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 }
40	38 39	nfriota	⊢ Ⅎ 𝑣 ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 )
41	37 40	nfmpt	⊢ Ⅎ 𝑣 ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
42	1 41	nfcxfr	⊢ Ⅎ 𝑣 𝐹
43		nfcv	⊢ Ⅎ 𝑣 𝑤
44	42 43	nffv	⊢ Ⅎ 𝑣 ( 𝐹 ‘ 𝑤 )
45	44	nfeq2	⊢ Ⅎ 𝑣 𝑢 = ( 𝐹 ‘ 𝑤 )
46		breq2	⊢ ( 𝑢 = ( 𝐹 ‘ 𝑤 ) → ( 𝑣 𝑅 𝑢 ↔ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
47	46	notbid	⊢ ( 𝑢 = ( 𝐹 ‘ 𝑤 ) → ( ¬ 𝑣 𝑅 𝑢 ↔ ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
48	45 47	ralbid	⊢ ( 𝑢 = ( 𝐹 ‘ 𝑤 ) → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ↔ ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
49	30 36 48	riota2f	⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∧ ∃! 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ↔ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) = ( 𝐹 ‘ 𝑤 ) ) )
50	16 8 49	syl2anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ↔ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) = ( 𝐹 ‘ 𝑤 ) ) )
51	24 50	mpbird	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) )
52	17	elrabsf	⊢ ( 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ↔ ( 𝑣 ∈ 𝐴 ∧ [ 𝑣 / 𝑥 ] 𝑤 ∈ 𝐵 ) )
53		sbcel2	⊢ ( [ 𝑣 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 )
54	53	anbi2i	⊢ ( ( 𝑣 ∈ 𝐴 ∧ [ 𝑣 / 𝑥 ] 𝑤 ∈ 𝐵 ) ↔ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 ) )
55	52 54	bitri	⊢ ( 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ↔ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 ) )
56	55	imbi1i	⊢ ( ( 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ↔ ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 ) → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
57		impexp	⊢ ( ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 ) → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑣 ∈ 𝐴 → ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
58	56 57	bitri	⊢ ( ( 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑣 ∈ 𝐴 → ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
59	58	ralbii2	⊢ ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
60	51 59	sylib	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
61	60	ralrimiva	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
62	12 23 61	3jca	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )