Metamath Proof Explorer

Theorem fin23lem28

Description: Lemma for fin23 . The residual is also one-to-one. This preserves the induction invariant. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem.a ⊢ U = seq ω i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u ⋃ ran ⁡ t
fin23lem17.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
fin23lem.b ⊢ P = v ∈ ω | ⋂ ran ⁡ U ⊆ t ⁡ v
fin23lem.c ⊢ Q = w ∈ ω ⟼ ι x ∈ P | x ∩ P ≈ w
fin23lem.d ⊢ R = w ∈ ω ⟼ ι x ∈ ω ∖ P | x ∩ ω ∖ P ≈ w
fin23lem.e ⊢ Z = if P ∈ Fin t ∘ R z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
Assertion fin23lem28 ⊢ t : ω ⟶ 1-1 V → Z : ω ⟶ 1-1 V

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ U = seq ω i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u ⋃ ran ⁡ t
2 fin23lem17.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
3 fin23lem.b ⊢ P = v ∈ ω | ⋂ ran ⁡ U ⊆ t ⁡ v
4 fin23lem.c ⊢ Q = w ∈ ω ⟼ ι x ∈ P | x ∩ P ≈ w
5 fin23lem.d ⊢ R = w ∈ ω ⟼ ι x ∈ ω ∖ P | x ∩ ω ∖ P ≈ w
6 fin23lem.e ⊢ Z = if P ∈ Fin t ∘ R z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
7 eqif ⊢ Z = if P ∈ Fin t ∘ R z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q ↔ P ∈ Fin ∧ Z = t ∘ R ∨ ¬ P ∈ Fin ∧ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
8 6 7 mpbi ⊢ P ∈ Fin ∧ Z = t ∘ R ∨ ¬ P ∈ Fin ∧ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
9 difss ⊢ ω ∖ P ⊆ ω
10 ominf ⊢ ¬ ω ∈ Fin
11 3 ssrab3 ⊢ P ⊆ ω
12 undif ⊢ P ⊆ ω ↔ P ∪ ω ∖ P = ω
13 11 12 mpbi ⊢ P ∪ ω ∖ P = ω
14 unfi ⊢ P ∈ Fin ∧ ω ∖ P ∈ Fin → P ∪ ω ∖ P ∈ Fin
15 13 14 eqeltrrid ⊢ P ∈ Fin ∧ ω ∖ P ∈ Fin → ω ∈ Fin
16 15 ex ⊢ P ∈ Fin → ω ∖ P ∈ Fin → ω ∈ Fin
17 10 16 mtoi ⊢ P ∈ Fin → ¬ ω ∖ P ∈ Fin
18 5 fin23lem22 ⊢ ω ∖ P ⊆ ω ∧ ¬ ω ∖ P ∈ Fin → R : ω ⟶ 1-1 onto ω ∖ P
19 9 17 18 sylancr ⊢ P ∈ Fin → R : ω ⟶ 1-1 onto ω ∖ P
20 19 adantl ⊢ t : ω ⟶ 1-1 V ∧ P ∈ Fin → R : ω ⟶ 1-1 onto ω ∖ P
21 f1of1 ⊢ R : ω ⟶ 1-1 onto ω ∖ P → R : ω ⟶ 1-1 ω ∖ P
22 f1ss ⊢ R : ω ⟶ 1-1 ω ∖ P ∧ ω ∖ P ⊆ ω → R : ω ⟶ 1-1 ω
23 9 22 mpan2 ⊢ R : ω ⟶ 1-1 ω ∖ P → R : ω ⟶ 1-1 ω
24 20 21 23 3syl ⊢ t : ω ⟶ 1-1 V ∧ P ∈ Fin → R : ω ⟶ 1-1 ω
25 f1co ⊢ t : ω ⟶ 1-1 V ∧ R : ω ⟶ 1-1 ω → t ∘ R : ω ⟶ 1-1 V
26 24 25 syldan ⊢ t : ω ⟶ 1-1 V ∧ P ∈ Fin → t ∘ R : ω ⟶ 1-1 V
27 f1eq1 ⊢ Z = t ∘ R → Z : ω ⟶ 1-1 V ↔ t ∘ R : ω ⟶ 1-1 V
28 26 27 syl5ibrcom ⊢ t : ω ⟶ 1-1 V ∧ P ∈ Fin → Z = t ∘ R → Z : ω ⟶ 1-1 V
29 28 impr ⊢ t : ω ⟶ 1-1 V ∧ P ∈ Fin ∧ Z = t ∘ R → Z : ω ⟶ 1-1 V
30 fvex ⊢ t ⁡ z ∈ V
31 30 difexi ⊢ t ⁡ z ∖ ⋂ ran ⁡ U ∈ V
32 31 rgenw ⊢ ∀ z ∈ P t ⁡ z ∖ ⋂ ran ⁡ U ∈ V
33 eqid ⊢ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U
34 33 fmpt ⊢ ∀ z ∈ P t ⁡ z ∖ ⋂ ran ⁡ U ∈ V ↔ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U : P ⟶ V
35 32 34 mpbi ⊢ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U : P ⟶ V
36 35 a1i ⊢ t : ω ⟶ 1-1 V → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U : P ⟶ V
37 fveq2 ⊢ z = a → t ⁡ z = t ⁡ a
38 37 difeq1d ⊢ z = a → t ⁡ z ∖ ⋂ ran ⁡ U = t ⁡ a ∖ ⋂ ran ⁡ U
39 fvex ⊢ t ⁡ a ∈ V
40 39 difexi ⊢ t ⁡ a ∖ ⋂ ran ⁡ U ∈ V
41 38 33 40 fvmpt ⊢ a ∈ P → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ a = t ⁡ a ∖ ⋂ ran ⁡ U
42 41 ad2antrl ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ a = t ⁡ a ∖ ⋂ ran ⁡ U
43 fveq2 ⊢ z = b → t ⁡ z = t ⁡ b
44 43 difeq1d ⊢ z = b → t ⁡ z ∖ ⋂ ran ⁡ U = t ⁡ b ∖ ⋂ ran ⁡ U
45 fvex ⊢ t ⁡ b ∈ V
46 45 difexi ⊢ t ⁡ b ∖ ⋂ ran ⁡ U ∈ V
47 44 33 46 fvmpt ⊢ b ∈ P → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ b = t ⁡ b ∖ ⋂ ran ⁡ U
48 47 ad2antll ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ b = t ⁡ b ∖ ⋂ ran ⁡ U
49 42 48 eqeq12d ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ a = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ b ↔ t ⁡ a ∖ ⋂ ran ⁡ U = t ⁡ b ∖ ⋂ ran ⁡ U
50 uneq2 ⊢ t ⁡ a ∖ ⋂ ran ⁡ U = t ⁡ b ∖ ⋂ ran ⁡ U → ⋂ ran ⁡ U ∪ t ⁡ a ∖ ⋂ ran ⁡ U = ⋂ ran ⁡ U ∪ t ⁡ b ∖ ⋂ ran ⁡ U
51 fveq2 ⊢ v = a → t ⁡ v = t ⁡ a
52 51 sseq2d ⊢ v = a → ⋂ ran ⁡ U ⊆ t ⁡ v ↔ ⋂ ran ⁡ U ⊆ t ⁡ a
53 52 3 elrab2 ⊢ a ∈ P ↔ a ∈ ω ∧ ⋂ ran ⁡ U ⊆ t ⁡ a
54 53 simprbi ⊢ a ∈ P → ⋂ ran ⁡ U ⊆ t ⁡ a
55 54 ad2antrl ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → ⋂ ran ⁡ U ⊆ t ⁡ a
56 undif ⊢ ⋂ ran ⁡ U ⊆ t ⁡ a ↔ ⋂ ran ⁡ U ∪ t ⁡ a ∖ ⋂ ran ⁡ U = t ⁡ a
57 55 56 sylib ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → ⋂ ran ⁡ U ∪ t ⁡ a ∖ ⋂ ran ⁡ U = t ⁡ a
58 fveq2 ⊢ v = b → t ⁡ v = t ⁡ b
59 58 sseq2d ⊢ v = b → ⋂ ran ⁡ U ⊆ t ⁡ v ↔ ⋂ ran ⁡ U ⊆ t ⁡ b
60 59 3 elrab2 ⊢ b ∈ P ↔ b ∈ ω ∧ ⋂ ran ⁡ U ⊆ t ⁡ b
61 60 simprbi ⊢ b ∈ P → ⋂ ran ⁡ U ⊆ t ⁡ b
62 61 ad2antll ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → ⋂ ran ⁡ U ⊆ t ⁡ b
63 undif ⊢ ⋂ ran ⁡ U ⊆ t ⁡ b ↔ ⋂ ran ⁡ U ∪ t ⁡ b ∖ ⋂ ran ⁡ U = t ⁡ b
64 62 63 sylib ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → ⋂ ran ⁡ U ∪ t ⁡ b ∖ ⋂ ran ⁡ U = t ⁡ b
65 57 64 eqeq12d ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → ⋂ ran ⁡ U ∪ t ⁡ a ∖ ⋂ ran ⁡ U = ⋂ ran ⁡ U ∪ t ⁡ b ∖ ⋂ ran ⁡ U ↔ t ⁡ a = t ⁡ b
66 50 65 syl5ib ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → t ⁡ a ∖ ⋂ ran ⁡ U = t ⁡ b ∖ ⋂ ran ⁡ U → t ⁡ a = t ⁡ b
67 11 sseli ⊢ a ∈ P → a ∈ ω
68 11 sseli ⊢ b ∈ P → b ∈ ω
69 67 68 anim12i ⊢ a ∈ P ∧ b ∈ P → a ∈ ω ∧ b ∈ ω
70 f1fveq ⊢ t : ω ⟶ 1-1 V ∧ a ∈ ω ∧ b ∈ ω → t ⁡ a = t ⁡ b ↔ a = b
71 69 70 sylan2 ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → t ⁡ a = t ⁡ b ↔ a = b
72 66 71 sylibd ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → t ⁡ a ∖ ⋂ ran ⁡ U = t ⁡ b ∖ ⋂ ran ⁡ U → a = b
73 49 72 sylbid ⊢ t : ω ⟶ 1-1 V ∧ a ∈ P ∧ b ∈ P → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ a = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ b → a = b
74 73 ralrimivva ⊢ t : ω ⟶ 1-1 V → ∀ a ∈ P ∀ b ∈ P z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ a = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ b → a = b
75 dff13 ⊢ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U : P ⟶ 1-1 V ↔ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U : P ⟶ V ∧ ∀ a ∈ P ∀ b ∈ P z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ a = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⁡ b → a = b
76 36 74 75 sylanbrc ⊢ t : ω ⟶ 1-1 V → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U : P ⟶ 1-1 V
77 4 fin23lem22 ⊢ P ⊆ ω ∧ ¬ P ∈ Fin → Q : ω ⟶ 1-1 onto P
78 f1of1 ⊢ Q : ω ⟶ 1-1 onto P → Q : ω ⟶ 1-1 P
79 77 78 syl ⊢ P ⊆ ω ∧ ¬ P ∈ Fin → Q : ω ⟶ 1-1 P
80 11 79 mpan ⊢ ¬ P ∈ Fin → Q : ω ⟶ 1-1 P
81 f1co ⊢ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U : P ⟶ 1-1 V ∧ Q : ω ⟶ 1-1 P → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q : ω ⟶ 1-1 V
82 76 80 81 syl2an ⊢ t : ω ⟶ 1-1 V ∧ ¬ P ∈ Fin → z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q : ω ⟶ 1-1 V
83 f1eq1 ⊢ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → Z : ω ⟶ 1-1 V ↔ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q : ω ⟶ 1-1 V
84 82 83 syl5ibrcom ⊢ t : ω ⟶ 1-1 V ∧ ¬ P ∈ Fin → Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → Z : ω ⟶ 1-1 V
85 84 impr ⊢ t : ω ⟶ 1-1 V ∧ ¬ P ∈ Fin ∧ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → Z : ω ⟶ 1-1 V
86 29 85 jaodan ⊢ t : ω ⟶ 1-1 V ∧ P ∈ Fin ∧ Z = t ∘ R ∨ ¬ P ∈ Fin ∧ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → Z : ω ⟶ 1-1 V
87 8 86 mpan2 ⊢ t : ω ⟶ 1-1 V → Z : ω ⟶ 1-1 V