Metamath Proof Explorer

Theorem weiunfrlem

Description: Lemma for weiunfr . (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
weiunfrlem.5 ⊢ E = ι p ∈ F r | ∀ q ∈ F r ¬ q R p
weiunfrlem.6 ⊢ φ → r ⊆ ⋃ x ∈ A B
weiunfrlem.7 ⊢ φ → r ≠ ∅
Assertion weiunfrlem ⊢ φ → E ∈ F r ∧ ∀ t ∈ r ¬ F ⁡ t R E ∧ ∀ t ∈ r ∩ ⦋ E / x⦌ B F ⁡ t = E

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 weiunfrlem.5 ⊢ E = ι p ∈ F r | ∀ q ∈ F r ¬ q R p
6 weiunfrlem.6 ⊢ φ → r ⊆ ⋃ x ∈ A B
7 weiunfrlem.7 ⊢ φ → r ≠ ∅
8 1 2 3 4 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
9 8 simp1d ⊢ φ → F : ⋃ x ∈ A B ⟶ A
10 9 fimassd ⊢ φ → F r ⊆ A
11 9 fdmd ⊢ φ → dom ⁡ F = ⋃ x ∈ A B
12 6 11 sseqtrrd ⊢ φ → r ⊆ dom ⁡ F
13 sseqin2 ⊢ r ⊆ dom ⁡ F ↔ dom ⁡ F ∩ r = r
14 12 13 sylib ⊢ φ → dom ⁡ F ∩ r = r
15 14 7 eqnetrd ⊢ φ → dom ⁡ F ∩ r ≠ ∅
16 15 imadisjlnd ⊢ φ → F r ≠ ∅
17 wereu2 ⊢ R We A ∧ R Se A ∧ F r ⊆ A ∧ F r ≠ ∅ → ∃! p ∈ F r ∀ q ∈ F r ¬ q R p
18 3 4 10 16 17 syl22anc ⊢ φ → ∃! p ∈ F r ∀ q ∈ F r ¬ q R p
19 riotacl2 ⊢ ∃! p ∈ F r ∀ q ∈ F r ¬ q R p → ι p ∈ F r | ∀ q ∈ F r ¬ q R p ∈ p ∈ F r | ∀ q ∈ F r ¬ q R p
20 18 19 syl ⊢ φ → ι p ∈ F r | ∀ q ∈ F r ¬ q R p ∈ p ∈ F r | ∀ q ∈ F r ¬ q R p
21 simpr ⊢ n = p ∧ o = q → o = q
22 simpl ⊢ n = p ∧ o = q → n = p
23 21 22 breq12d ⊢ n = p ∧ o = q → o R n ↔ q R p
24 23 notbid ⊢ n = p ∧ o = q → ¬ o R n ↔ ¬ q R p
25 24 cbvraldva ⊢ n = p → ∀ o ∈ F r ¬ o R n ↔ ∀ q ∈ F r ¬ q R p
26 25 cbvrabv ⊢ n ∈ F r | ∀ o ∈ F r ¬ o R n = p ∈ F r | ∀ q ∈ F r ¬ q R p
27 20 5 26 3eltr4g ⊢ φ → E ∈ n ∈ F r | ∀ o ∈ F r ¬ o R n
28 breq2 ⊢ n = E → o R n ↔ o R E
29 28 notbid ⊢ n = E → ¬ o R n ↔ ¬ o R E
30 29 ralbidv ⊢ n = E → ∀ o ∈ F r ¬ o R n ↔ ∀ o ∈ F r ¬ o R E
31 30 elrab ⊢ E ∈ n ∈ F r | ∀ o ∈ F r ¬ o R n ↔ E ∈ F r ∧ ∀ o ∈ F r ¬ o R E
32 27 31 sylib ⊢ φ → E ∈ F r ∧ ∀ o ∈ F r ¬ o R E
33 32 simpld ⊢ φ → E ∈ F r
34 32 simprd ⊢ φ → ∀ o ∈ F r ¬ o R E
35 9 ffnd ⊢ φ → F Fn ⋃ x ∈ A B
36 breq1 ⊢ o = F ⁡ t → o R E ↔ F ⁡ t R E
37 36 notbid ⊢ o = F ⁡ t → ¬ o R E ↔ ¬ F ⁡ t R E
38 37 ralima ⊢ F Fn ⋃ x ∈ A B ∧ r ⊆ ⋃ x ∈ A B → ∀ o ∈ F r ¬ o R E ↔ ∀ t ∈ r ¬ F ⁡ t R E
39 35 6 38 syl2anc ⊢ φ → ∀ o ∈ F r ¬ o R E ↔ ∀ t ∈ r ¬ F ⁡ t R E
40 34 39 mpbid ⊢ φ → ∀ t ∈ r ¬ F ⁡ t R E
41 simpr ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → t ∈ r ∩ ⦋ E / x⦌ B
42 41 elin1d ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → t ∈ r
43 rspa ⊢ ∀ t ∈ r ¬ F ⁡ t R E ∧ t ∈ r → ¬ F ⁡ t R E
44 40 42 43 syl2an2r ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → ¬ F ⁡ t R E
45 csbeq1 ⊢ s = E → ⦋ s / x⦌ B = ⦋ E / x⦌ B
46 breq1 ⊢ s = E → s R F ⁡ t ↔ E R F ⁡ t
47 46 notbid ⊢ s = E → ¬ s R F ⁡ t ↔ ¬ E R F ⁡ t
48 45 47 raleqbidv ⊢ s = E → ∀ t ∈ ⦋ s / x⦌ B ¬ s R F ⁡ t ↔ ∀ t ∈ ⦋ E / x⦌ B ¬ E R F ⁡ t
49 8 simp3d ⊢ φ → ∀ s ∈ A ∀ t ∈ ⦋ s / x⦌ B ¬ s R F ⁡ t
50 10 33 sseldd ⊢ φ → E ∈ A
51 48 49 50 rspcdva ⊢ φ → ∀ t ∈ ⦋ E / x⦌ B ¬ E R F ⁡ t
52 41 elin2d ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → t ∈ ⦋ E / x⦌ B
53 rspa ⊢ ∀ t ∈ ⦋ E / x⦌ B ¬ E R F ⁡ t ∧ t ∈ ⦋ E / x⦌ B → ¬ E R F ⁡ t
54 51 52 53 syl2an2r ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → ¬ E R F ⁡ t
55 weso ⊢ R We A → R Or A
56 3 55 syl ⊢ φ → R Or A
57 56 adantr ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → R Or A
58 9 adantr ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → F : ⋃ x ∈ A B ⟶ A
59 6 adantr ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → r ⊆ ⋃ x ∈ A B
60 59 42 sseldd ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → t ∈ ⋃ x ∈ A B
61 58 60 ffvelcdmd ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → F ⁡ t ∈ A
62 50 adantr ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → E ∈ A
63 sotrieq2 ⊢ R Or A ∧ F ⁡ t ∈ A ∧ E ∈ A → F ⁡ t = E ↔ ¬ F ⁡ t R E ∧ ¬ E R F ⁡ t
64 57 61 62 63 syl12anc ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → F ⁡ t = E ↔ ¬ F ⁡ t R E ∧ ¬ E R F ⁡ t
65 44 54 64 mpbir2and ⊢ φ ∧ t ∈ r ∩ ⦋ E / x⦌ B → F ⁡ t = E
66 65 ralrimiva ⊢ φ → ∀ t ∈ r ∩ ⦋ E / x⦌ B F ⁡ t = E
67 33 40 66 3jca ⊢ φ → E ∈ F r ∧ ∀ t ∈ r ¬ F ⁡ t R E ∧ ∀ t ∈ r ∩ ⦋ E / x⦌ B F ⁡ t = E