Metamath Proof Explorer


Theorem weiunlem2

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

Ref Expression
Hypotheses weiun.1 F = w x A B ι u x A | w B | v x A | w B ¬ v R u
weiun.2 T = y z | y x A B z x A B F y R F z F y = F z y F y / x S z
weiunlem2.3 φ R We A
weiunlem2.4 φ R Se A
Assertion weiunlem2 φ F : x A B A t x A B t F t / x B s A t s / x B ¬ s R F t

Proof

Step Hyp Ref Expression
1 weiun.1 F = w x A B ι u x A | w B | v x A | w B ¬ v R u
2 weiun.2 T = y z | y x A B z x A B F y R F z F y = F z y F y / x S z
3 weiunlem2.3 φ R We A
4 weiunlem2.4 φ R Se A
5 riotaex ι u x A | w B | v x A | w B ¬ v R u V
6 5 1 fnmpti F Fn x A B
7 6 a1i R We A R Se A F Fn x A B
8 breq2 u = r v R u v R r
9 8 notbid u = r ¬ v R u ¬ v R r
10 9 ralbidv u = r v x A | w B ¬ v R u v x A | w B ¬ v R r
11 10 cbvriotavw ι u x A | w B | v x A | w B ¬ v R u = ι r x A | w B | v x A | w B ¬ v R r
12 eleq1w w = t w B t B
13 12 rabbidv w = t x A | w B = x A | t B
14 breq1 v = s v R r s R r
15 14 notbid v = s ¬ v R r ¬ s R r
16 15 cbvralvw v x A | w B ¬ v R r s x A | w B ¬ s R r
17 13 raleqdv w = t s x A | w B ¬ s R r s x A | t B ¬ s R r
18 16 17 bitrid w = t v x A | w B ¬ v R r s x A | t B ¬ s R r
19 13 18 riotaeqbidv w = t ι r x A | w B | v x A | w B ¬ v R r = ι r x A | t B | s x A | t B ¬ s R r
20 11 19 eqtrid w = t ι u x A | w B | v x A | w B ¬ v R u = ι r x A | t B | s x A | t B ¬ s R r
21 20 1 5 fvmpt3i t x A B F t = ι r x A | t B | s x A | t B ¬ s R r
22 21 adantl R We A R Se A t x A B F t = ι r x A | t B | s x A | t B ¬ s R r
23 eliun t x A B x A t B
24 rabn0 x A | t B x A t B
25 23 24 bitr4i t x A B x A | t B
26 ssrab2 x A | t B A
27 wereu2 R We A R Se A x A | t B A x A | t B ∃! r x A | t B s x A | t B ¬ s R r
28 26 27 mpanr1 R We A R Se A x A | t B ∃! r x A | t B s x A | t B ¬ s R r
29 25 28 sylan2b R We A R Se A t x A B ∃! r x A | t B s x A | t B ¬ s R r
30 riotacl2 ∃! r x A | t B s x A | t B ¬ s R r ι r x A | t B | s x A | t B ¬ s R r r x A | t B | s x A | t B ¬ s R r
31 29 30 syl R We A R Se A t x A B ι r x A | t B | s x A | t B ¬ s R r r x A | t B | s x A | t B ¬ s R r
32 22 31 eqeltrd R We A R Se A t x A B F t r x A | t B | s x A | t B ¬ s R r
33 elrabi F t r x A | t B | s x A | t B ¬ s R r F t x A | t B
34 elrabi F t x A | t B F t A
35 32 33 34 3syl R We A R Se A t x A B F t A
36 35 ralrimiva R We A R Se A t x A B F t A
37 ffnfv F : x A B A F Fn x A B t x A B F t A
38 7 36 37 sylanbrc R We A R Se A F : x A B A
39 dfsbcq s = F t [˙s / x]˙ t B [˙ F t / x]˙ t B
40 nfcv _ x A
41 40 elrabsf s x A | t B s A [˙s / x]˙ t B
42 41 simprbi s x A | t B [˙s / x]˙ t B
43 39 42 vtoclga F t x A | t B [˙ F t / x]˙ t B
44 32 33 43 3syl R We A R Se A t x A B [˙ F t / x]˙ t B
45 sbcel2 [˙ F t / x]˙ t B t F t / x B
46 44 45 sylib R We A R Se A t x A B t F t / x B
47 46 ralrimiva R We A R Se A t x A B t F t / x B
48 simpr R We A R Se A s A t s / x B s A t s / x B
49 sbcel2 [˙s / x]˙ t B t s / x B
50 49 anbi2i s A [˙s / x]˙ t B s A t s / x B
51 41 50 bitri s x A | t B s A t s / x B
52 48 51 sylibr R We A R Se A s A t s / x B s x A | t B
53 52 ne0d R We A R Se A s A t s / x B x A | t B
54 53 25 sylibr R We A R Se A s A t s / x B t x A B
55 breq2 r = F t s R r s R F t
56 55 notbid r = F t ¬ s R r ¬ s R F t
57 56 ralbidv r = F t s x A | t B ¬ s R r s x A | t B ¬ s R F t
58 57 elrab F t r x A | t B | s x A | t B ¬ s R r F t x A | t B s x A | t B ¬ s R F t
59 58 simprbi F t r x A | t B | s x A | t B ¬ s R r s x A | t B ¬ s R F t
60 32 59 syl R We A R Se A t x A B s x A | t B ¬ s R F t
61 54 60 syldan R We A R Se A s A t s / x B s x A | t B ¬ s R F t
62 rsp s x A | t B ¬ s R F t s x A | t B ¬ s R F t
63 61 52 62 sylc R We A R Se A s A t s / x B ¬ s R F t
64 63 ralrimivva R We A R Se A s A t s / x B ¬ s R F t
65 38 47 64 3jca R We A R Se A F : x A B A t x A B t F t / x B s A t s / x B ¬ s R F t
66 3 4 65 syl2anc φ F : x A B A t x A B t F t / x B s A t s / x B ¬ s R F t