Theorem weiunlem1

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

	Ref	Expression
Hypothesis	weiunlem1.1	|- F = ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
Assertion	weiunlem1	|- ( ( R We A /\ R Se A ) -> ( F : U_ x e. A B --> A /\ A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B /\ A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		weiunlem1.1	|- F = ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
2		ssrab2	|- { x e. A | w e. B } C_ A
3		eliun	|- ( w e. U_ x e. A B <-> E. x e. A w e. B )
4		rabn0	|- ( { x e. A | w e. B } =/= (/) <-> E. x e. A w e. B )
5	3 4	sylbb2	|- ( w e. U_ x e. A B -> { x e. A | w e. B } =/= (/) )
6		wereu2	|- ( ( ( R We A /\ R Se A ) /\ ( { x e. A | w e. B } C_ A /\ { x e. A | w e. B } =/= (/) ) ) -> E! u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u )
7	2 6	mpanr1	|- ( ( ( R We A /\ R Se A ) /\ { x e. A | w e. B } =/= (/) ) -> E! u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u )
8	5 7	sylan2	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> E! u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u )
9		riotacl	|- ( E! u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u -> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) e. { x e. A | w e. B } )
10	8 9	syl	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) e. { x e. A | w e. B } )
11	2 10	sselid	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) e. A )
12	11 1	fmptd	|- ( ( R We A /\ R Se A ) -> F : U_ x e. A B --> A )
13		simpr	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> w e. U_ x e. A B )
14	1	fvmpt2	|- ( ( w e. U_ x e. A B /\ ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) e. { x e. A | w e. B } ) -> ( F ` w ) = ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
15	13 10 14	syl2anc	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> ( F ` w ) = ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
16	15 10	eqeltrd	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> ( F ` w ) e. { x e. A | w e. B } )
17		nfcv	|- F/_ x A
18	17	elrabsf	|- ( ( F ` w ) e. { x e. A | w e. B } <-> ( ( F ` w ) e. A /\ [. ( F ` w ) / x ]. w e. B ) )
19	16 18	sylib	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> ( ( F ` w ) e. A /\ [. ( F ` w ) / x ]. w e. B ) )
20	19	simprd	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> [. ( F ` w ) / x ]. w e. B )
21		sbcel2	|- ( [. ( F ` w ) / x ]. w e. B <-> w e. [_ ( F ` w ) / x ]_ B )
22	20 21	sylib	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> w e. [_ ( F ` w ) / x ]_ B )
23	22	ralrimiva	|- ( ( R We A /\ R Se A ) -> A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B )
24	15	eqcomd	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) = ( F ` w ) )
25		nfcv	|- F/_ u U_ x e. A B
26		nfriota1	|- F/_ u ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u )
27	25 26	nfmpt	|- F/_ u ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
28	1 27	nfcxfr	|- F/_ u F
29		nfcv	|- F/_ u w
30	28 29	nffv	|- F/_ u ( F ` w )
31		nfcv	|- F/_ u { x e. A | w e. B }
32		nfcv	|- F/_ u v
33		nfcv	|- F/_ u R
34	32 33 30	nfbr	|- F/ u v R ( F ` w )
35	34	nfn	|- F/ u -. v R ( F ` w )
36	31 35	nfralw	|- F/ u A. v e. { x e. A | w e. B } -. v R ( F ` w )
37		nfcv	|- F/_ v U_ x e. A B
38		nfra1	|- F/ v A. v e. { x e. A | w e. B } -. v R u
39		nfcv	|- F/_ v { x e. A | w e. B }
40	38 39	nfriota	|- F/_ v ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u )
41	37 40	nfmpt	|- F/_ v ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
42	1 41	nfcxfr	|- F/_ v F
43		nfcv	|- F/_ v w
44	42 43	nffv	|- F/_ v ( F ` w )
45	44	nfeq2	|- F/ v u = ( F ` w )
46		breq2	|- ( u = ( F ` w ) -> ( v R u <-> v R ( F ` w ) ) )
47	46	notbid	|- ( u = ( F ` w ) -> ( -. v R u <-> -. v R ( F ` w ) ) )
48	45 47	ralbid	|- ( u = ( F ` w ) -> ( A. v e. { x e. A | w e. B } -. v R u <-> A. v e. { x e. A | w e. B } -. v R ( F ` w ) ) )
49	30 36 48	riota2f	|- ( ( ( F ` w ) e. { x e. A | w e. B } /\ E! u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) -> ( A. v e. { x e. A | w e. B } -. v R ( F ` w ) <-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) = ( F ` w ) ) )
50	16 8 49	syl2anc	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> ( A. v e. { x e. A | w e. B } -. v R ( F ` w ) <-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) = ( F ` w ) ) )
51	24 50	mpbird	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> A. v e. { x e. A | w e. B } -. v R ( F ` w ) )
52	17	elrabsf	|- ( v e. { x e. A | w e. B } <-> ( v e. A /\ [. v / x ]. w e. B ) )
53		sbcel2	|- ( [. v / x ]. w e. B <-> w e. [_ v / x ]_ B )
54	53	anbi2i	|- ( ( v e. A /\ [. v / x ]. w e. B ) <-> ( v e. A /\ w e. [_ v / x ]_ B ) )
55	52 54	bitri	|- ( v e. { x e. A | w e. B } <-> ( v e. A /\ w e. [_ v / x ]_ B ) )
56	55	imbi1i	|- ( ( v e. { x e. A | w e. B } -> -. v R ( F ` w ) ) <-> ( ( v e. A /\ w e. [_ v / x ]_ B ) -> -. v R ( F ` w ) ) )
57		impexp	|- ( ( ( v e. A /\ w e. [_ v / x ]_ B ) -> -. v R ( F ` w ) ) <-> ( v e. A -> ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )
58	56 57	bitri	|- ( ( v e. { x e. A | w e. B } -> -. v R ( F ` w ) ) <-> ( v e. A -> ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )
59	58	ralbii2	|- ( A. v e. { x e. A | w e. B } -. v R ( F ` w ) <-> A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) )
60	51 59	sylib	|- ( ( ( R We A /\ R Se A ) /\ w e. U_ x e. A B ) -> A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) )
61	60	ralrimiva	|- ( ( R We A /\ R Se A ) -> A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) )
62	12 23 61	3jca	|- ( ( R We A /\ R Se A ) -> ( F : U_ x e. A B --> A /\ A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B /\ A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )