Metamath Proof Explorer

Theorem weiunlem

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
weiunlem.3 ⊢ φ → R We A
weiunlem.4 ⊢ φ → R Se A
Assertion weiunlem ⊢ φ → 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 weiunlem.3 ⊢ φ → R We A
4 weiunlem.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 sbcel2 ⊢ [˙s / x]˙ t ∈ B ↔ t ∈ ⦋ s / x⦌ B
49 48 anbi2i ⊢ s ∈ A ∧ [˙s / x]˙ t ∈ B ↔ s ∈ A ∧ t ∈ ⦋ s / x⦌ B
50 41 49 bitri ⊢ s ∈ x ∈ A | t ∈ B ↔ s ∈ A ∧ t ∈ ⦋ s / x⦌ B
51 50 bilanri ⊢ R We A ∧ R Se A ∧ s ∈ A ∧ t ∈ ⦋ s / x⦌ B → s ∈ x ∈ A | t ∈ B
52 51 ne0d ⊢ R We A ∧ R Se A ∧ s ∈ A ∧ t ∈ ⦋ s / x⦌ B → x ∈ A | t ∈ B ≠ ∅
53 52 25 sylibr ⊢ R We A ∧ R Se A ∧ s ∈ A ∧ t ∈ ⦋ s / x⦌ B → t ∈ ⋃ x ∈ A B
54 breq2 ⊢ r = F ⁡ t → s R r ↔ s R F ⁡ t
55 54 notbid ⊢ r = F ⁡ t → ¬ s R r ↔ ¬ s R F ⁡ t
56 55 ralbidv ⊢ r = F ⁡ t → ∀ s ∈ x ∈ A | t ∈ B ¬ s R r ↔ ∀ s ∈ x ∈ A | t ∈ B ¬ s R F ⁡ t
57 56 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
58 57 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
59 32 58 syl ⊢ R We A ∧ R Se A ∧ t ∈ ⋃ x ∈ A B → ∀ s ∈ x ∈ A | t ∈ B ¬ s R F ⁡ t
60 53 59 syldan ⊢ R We A ∧ R Se A ∧ s ∈ A ∧ t ∈ ⦋ s / x⦌ B → ∀ s ∈ x ∈ A | t ∈ B ¬ s R F ⁡ t
61 rsp ⊢ ∀ s ∈ x ∈ A | t ∈ B ¬ s R F ⁡ t → s ∈ x ∈ A | t ∈ B → ¬ s R F ⁡ t
62 60 51 61 sylc ⊢ R We A ∧ R Se A ∧ s ∈ A ∧ t ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ t
63 62 ralrimivva ⊢ R We A ∧ R Se A → ∀ s ∈ A ∀ t ∈ ⦋ s / x⦌ B ¬ s R F ⁡ t
64 38 47 63 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
65 3 4 64 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