Metamath Proof Explorer

Theorem weiunlem1

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

Ref Expression
Hypothesis weiunlem1.1 ⊢ F = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
Assertion weiunlem1 ⊢ R We A ∧ R Se A → F : ⋃ x ∈ A B ⟶ A ∧ ∀ w ∈ ⋃ x ∈ A B w ∈ ⦋ F ⁡ w / x⦌ B ∧ ∀ w ∈ ⋃ x ∈ A B ∀ v ∈ A w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w

Proof

Step Hyp Ref Expression
1 weiunlem1.1 ⊢ F = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
2 ssrab2 ⊢ x ∈ A | w ∈ B ⊆ A
3 eliun ⊢ w ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A w ∈ B
4 rabn0 ⊢ x ∈ A | w ∈ B ≠ ∅ ↔ ∃ x ∈ A w ∈ B
5 3 4 sylbb2 ⊢ w ∈ ⋃ x ∈ A B → x ∈ A | w ∈ B ≠ ∅
6 wereu2 ⊢ R We A ∧ R Se A ∧ x ∈ A | w ∈ B ⊆ A ∧ x ∈ A | w ∈ B ≠ ∅ → ∃! u ∈ x ∈ A | w ∈ B ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
7 2 6 mpanr1 ⊢ R We A ∧ R Se A ∧ x ∈ A | w ∈ B ≠ ∅ → ∃! u ∈ x ∈ A | w ∈ B ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
8 5 7 sylan2 ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → ∃! u ∈ x ∈ A | w ∈ B ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
9 riotacl ⊢ ∃! u ∈ x ∈ A | w ∈ B ∀ v ∈ x ∈ A | w ∈ B ¬ v R u → ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u ∈ x ∈ A | w ∈ B
10 8 9 syl ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u ∈ x ∈ A | w ∈ B
11 2 10 sselid ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u ∈ A
12 11 1 fmptd ⊢ R We A ∧ R Se A → F : ⋃ x ∈ A B ⟶ A
13 simpr ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → w ∈ ⋃ x ∈ A B
14 1 fvmpt2 ⊢ w ∈ ⋃ x ∈ A B ∧ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u ∈ x ∈ A | w ∈ B → F ⁡ w = ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
15 13 10 14 syl2anc ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → F ⁡ w = ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
16 15 10 eqeltrd ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → F ⁡ w ∈ x ∈ A | w ∈ B
17 nfcv ⊢ Ⅎ _ x A
18 17 elrabsf ⊢ F ⁡ w ∈ x ∈ A | w ∈ B ↔ F ⁡ w ∈ A ∧ [˙ F ⁡ w / x]˙ w ∈ B
19 16 18 sylib ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → F ⁡ w ∈ A ∧ [˙ F ⁡ w / x]˙ w ∈ B
20 19 simprd ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → [˙ F ⁡ w / x]˙ w ∈ B
21 sbcel2 ⊢ [˙ F ⁡ w / x]˙ w ∈ B ↔ w ∈ ⦋ F ⁡ w / x⦌ B
22 20 21 sylib ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → w ∈ ⦋ F ⁡ w / x⦌ B
23 22 ralrimiva ⊢ R We A ∧ R Se A → ∀ w ∈ ⋃ x ∈ A B w ∈ ⦋ F ⁡ w / x⦌ B
24 15 eqcomd ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u = F ⁡ w
25 nfcv ⊢ Ⅎ _ u ⋃ x ∈ A B
26 nfriota1 ⊢ Ⅎ _ u ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
27 25 26 nfmpt ⊢ Ⅎ _ u w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
28 1 27 nfcxfr ⊢ Ⅎ _ u F
29 nfcv ⊢ Ⅎ _ u w
30 28 29 nffv ⊢ Ⅎ _ u F ⁡ w
31 nfcv ⊢ Ⅎ _ u x ∈ A | w ∈ B
32 nfcv ⊢ Ⅎ _ u v
33 nfcv ⊢ Ⅎ _ u R
34 32 33 30 nfbr ⊢ Ⅎ u v R F ⁡ w
35 34 nfn ⊢ Ⅎ u ¬ v R F ⁡ w
36 31 35 nfralw ⊢ Ⅎ u ∀ v ∈ x ∈ A | w ∈ B ¬ v R F ⁡ w
37 nfcv ⊢ Ⅎ _ v ⋃ x ∈ A B
38 nfra1 ⊢ Ⅎ v ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
39 nfcv ⊢ Ⅎ _ v x ∈ A | w ∈ B
40 38 39 nfriota ⊢ Ⅎ _ v ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
41 37 40 nfmpt ⊢ Ⅎ _ v w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
42 1 41 nfcxfr ⊢ Ⅎ _ v F
43 nfcv ⊢ Ⅎ _ v w
44 42 43 nffv ⊢ Ⅎ _ v F ⁡ w
45 44 nfeq2 ⊢ Ⅎ 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 → ∀ v ∈ x ∈ A | w ∈ B ¬ v R u ↔ ∀ v ∈ x ∈ A | w ∈ B ¬ v R F ⁡ w
49 30 36 48 riota2f ⊢ F ⁡ w ∈ x ∈ A | w ∈ B ∧ ∃! u ∈ x ∈ A | w ∈ B ∀ v ∈ x ∈ A | w ∈ B ¬ v R u → ∀ v ∈ x ∈ A | w ∈ B ¬ v R F ⁡ w ↔ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u = F ⁡ w
50 16 8 49 syl2anc ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → ∀ v ∈ x ∈ A | w ∈ B ¬ v R F ⁡ w ↔ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u = F ⁡ w
51 24 50 mpbird ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → ∀ v ∈ x ∈ A | w ∈ B ¬ v R F ⁡ w
52 17 elrabsf ⊢ v ∈ x ∈ A | w ∈ B ↔ v ∈ A ∧ [˙v / x]˙ w ∈ B
53 sbcel2 ⊢ [˙v / x]˙ w ∈ B ↔ w ∈ ⦋ v / x⦌ B
54 53 anbi2i ⊢ v ∈ A ∧ [˙v / x]˙ w ∈ B ↔ v ∈ A ∧ w ∈ ⦋ v / x⦌ B
55 52 54 bitri ⊢ v ∈ x ∈ A | w ∈ B ↔ v ∈ A ∧ w ∈ ⦋ v / x⦌ B
56 55 imbi1i ⊢ v ∈ x ∈ A | w ∈ B → ¬ v R F ⁡ w ↔ v ∈ A ∧ w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w
57 impexp ⊢ v ∈ A ∧ w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w ↔ v ∈ A → w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w
58 56 57 bitri ⊢ v ∈ x ∈ A | w ∈ B → ¬ v R F ⁡ w ↔ v ∈ A → w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w
59 58 ralbii2 ⊢ ∀ v ∈ x ∈ A | w ∈ B ¬ v R F ⁡ w ↔ ∀ v ∈ A w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w
60 51 59 sylib ⊢ R We A ∧ R Se A ∧ w ∈ ⋃ x ∈ A B → ∀ v ∈ A w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w
61 60 ralrimiva ⊢ R We A ∧ R Se A → ∀ w ∈ ⋃ x ∈ A B ∀ v ∈ A w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w
62 12 23 61 3jca ⊢ R We A ∧ R Se A → F : ⋃ x ∈ A B ⟶ A ∧ ∀ w ∈ ⋃ x ∈ A B w ∈ ⦋ F ⁡ w / x⦌ B ∧ ∀ w ∈ ⋃ x ∈ A B ∀ v ∈ A w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w