Metamath Proof Explorer

Theorem weiunlem2

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

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

Proof

Step Hyp Ref Expression
1 weiunlem2.1 ⊢ F = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
2 1 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
3 biid ⊢ F : ⋃ x ∈ A B ⟶ A ↔ F : ⋃ x ∈ A B ⟶ A
4 nfv ⊢ Ⅎ t w ∈ ⦋ F ⁡ w / x⦌ B
5 nfmpt1 ⊢ Ⅎ _ w w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
6 1 5 nfcxfr ⊢ Ⅎ _ w F
7 nfcv ⊢ Ⅎ _ w t
8 6 7 nffv ⊢ Ⅎ _ w F ⁡ t
9 nfcv ⊢ Ⅎ _ w B
10 8 9 nfcsbw ⊢ Ⅎ _ w ⦋ F ⁡ t / x⦌ B
11 10 nfcri ⊢ Ⅎ w t ∈ ⦋ F ⁡ t / x⦌ B
12 id ⊢ w = t → w = t
13 fveq2 ⊢ w = t → F ⁡ w = F ⁡ t
14 13 csbeq1d ⊢ w = t → ⦋ F ⁡ w / x⦌ B = ⦋ F ⁡ t / x⦌ B
15 12 14 eleq12d ⊢ w = t → w ∈ ⦋ F ⁡ w / x⦌ B ↔ t ∈ ⦋ F ⁡ t / x⦌ B
16 4 11 15 cbvralw ⊢ ∀ w ∈ ⋃ x ∈ A B w ∈ ⦋ F ⁡ w / x⦌ B ↔ ∀ t ∈ ⋃ x ∈ A B t ∈ ⦋ F ⁡ t / x⦌ B
17 nfv ⊢ Ⅎ t ∀ v ∈ A w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w
18 nfcv ⊢ Ⅎ _ w A
19 nfv ⊢ Ⅎ w t ∈ ⦋ s / x⦌ B
20 nfcv ⊢ Ⅎ _ w s
21 nfcv ⊢ Ⅎ _ w R
22 20 21 8 nfbr ⊢ Ⅎ w s R F ⁡ t
23 22 nfn ⊢ Ⅎ w ¬ s R F ⁡ t
24 19 23 nfim ⊢ Ⅎ w t ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ t
25 18 24 nfralw ⊢ Ⅎ w ∀ s ∈ A t ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ t
26 nfv ⊢ Ⅎ s w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w
27 nfv ⊢ Ⅎ v w ∈ ⦋ s / x⦌ B
28 nfcv ⊢ Ⅎ _ v s
29 nfcv ⊢ Ⅎ _ v R
30 nfcv ⊢ Ⅎ _ v ⋃ x ∈ A B
31 nfra1 ⊢ Ⅎ v ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
32 nfcv ⊢ Ⅎ _ v x ∈ A | w ∈ B
33 31 32 nfriota ⊢ Ⅎ _ v ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
34 30 33 nfmpt ⊢ Ⅎ _ v w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v R u
35 1 34 nfcxfr ⊢ Ⅎ _ v F
36 nfcv ⊢ Ⅎ _ v w
37 35 36 nffv ⊢ Ⅎ _ v F ⁡ w
38 28 29 37 nfbr ⊢ Ⅎ v s R F ⁡ w
39 38 nfn ⊢ Ⅎ v ¬ s R F ⁡ w
40 27 39 nfim ⊢ Ⅎ v w ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ w
41 csbeq1 ⊢ v = s → ⦋ v / x⦌ B = ⦋ s / x⦌ B
42 41 eleq2d ⊢ v = s → w ∈ ⦋ v / x⦌ B ↔ w ∈ ⦋ s / x⦌ B
43 breq1 ⊢ v = s → v R F ⁡ w ↔ s R F ⁡ w
44 43 notbid ⊢ v = s → ¬ v R F ⁡ w ↔ ¬ s R F ⁡ w
45 42 44 imbi12d ⊢ v = s → w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w ↔ w ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ w
46 26 40 45 cbvralw ⊢ ∀ v ∈ A w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w ↔ ∀ s ∈ A w ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ w
47 eleq1w ⊢ w = t → w ∈ ⦋ s / x⦌ B ↔ t ∈ ⦋ s / x⦌ B
48 13 breq2d ⊢ w = t → s R F ⁡ w ↔ s R F ⁡ t
49 48 notbid ⊢ w = t → ¬ s R F ⁡ w ↔ ¬ s R F ⁡ t
50 47 49 imbi12d ⊢ w = t → w ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ w ↔ t ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ t
51 50 ralbidv ⊢ w = t → ∀ s ∈ A w ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ w ↔ ∀ s ∈ A t ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ t
52 46 51 bitrid ⊢ w = t → ∀ v ∈ A w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w ↔ ∀ s ∈ A t ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ t
53 17 25 52 cbvralw ⊢ ∀ w ∈ ⋃ x ∈ A B ∀ v ∈ A w ∈ ⦋ v / x⦌ B → ¬ v R F ⁡ w ↔ ∀ t ∈ ⋃ x ∈ A B ∀ s ∈ A t ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ t
54 3 16 53 3anbi123i ⊢ 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 ↔ F : ⋃ x ∈ A B ⟶ A ∧ ∀ t ∈ ⋃ x ∈ A B t ∈ ⦋ F ⁡ t / x⦌ B ∧ ∀ t ∈ ⋃ x ∈ A B ∀ s ∈ A t ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ t
55 2 54 sylib ⊢ R We A ∧ R Se A → F : ⋃ x ∈ A B ⟶ A ∧ ∀ t ∈ ⋃ x ∈ A B t ∈ ⦋ F ⁡ t / x⦌ B ∧ ∀ t ∈ ⋃ x ∈ A B ∀ s ∈ A t ∈ ⦋ s / x⦌ B → ¬ s R F ⁡ t