Metamath Proof Explorer

Theorem onvf1odlem4

Description: Lemma for onvf1od . If the range of F does not exist, then it must equal the universe. (Contributed by BTernaryTau, 4-Dec-2025)

Ref Expression
Hypotheses onvf1odlem4.1 ⊢ φ → ∀ z z ≠ ∅ → G ⁡ z ∈ z
onvf1odlem4.2 ⊢ M = ⋂ x ∈ On | ∃ y ∈ R1 ⁡ x ¬ y ∈ ran ⁡ w
onvf1odlem4.3 ⊢ N = G ⁡ R1 ⁡ M ∖ ran ⁡ w
onvf1odlem4.4 ⊢ F = recs ⁡ w ∈ V ⟼ N
onvf1odlem4.5 ⊢ B = ⋂ u ∈ On | ∃ v ∈ R1 ⁡ u ¬ v ∈ F t
onvf1odlem4.6 ⊢ C = G ⁡ R1 ⁡ B ∖ F t
Assertion onvf1odlem4 ⊢ φ → ¬ ran ⁡ F ∈ V → ran ⁡ F = V

Proof

Step Hyp Ref Expression
1 onvf1odlem4.1 ⊢ φ → ∀ z z ≠ ∅ → G ⁡ z ∈ z
2 onvf1odlem4.2 ⊢ M = ⋂ x ∈ On | ∃ y ∈ R1 ⁡ x ¬ y ∈ ran ⁡ w
3 onvf1odlem4.3 ⊢ N = G ⁡ R1 ⁡ M ∖ ran ⁡ w
4 onvf1odlem4.4 ⊢ F = recs ⁡ w ∈ V ⟼ N
5 onvf1odlem4.5 ⊢ B = ⋂ u ∈ On | ∃ v ∈ R1 ⁡ u ¬ v ∈ F t
6 onvf1odlem4.6 ⊢ C = G ⁡ R1 ⁡ B ∖ F t
7 eqv ⊢ ran ⁡ F = V ↔ ∀ v v ∈ ran ⁡ F
8 exnal ⊢ ∃ v ¬ v ∈ ran ⁡ F ↔ ¬ ∀ v v ∈ ran ⁡ F
9 4 tfr1 ⊢ F Fn On
10 fvelrnb ⊢ F Fn On → s ∈ ran ⁡ F ↔ ∃ t ∈ On F ⁡ t = s
11 9 10 ax-mp ⊢ s ∈ ran ⁡ F ↔ ∃ t ∈ On F ⁡ t = s
12 2 3 4 5 6 onvf1odlem3 ⊢ t ∈ On → F ⁡ t = C
13 12 adantl ⊢ φ ∧ t ∈ On → F ⁡ t = C
14 fnfun ⊢ F Fn On → Fun ⁡ F
15 9 14 ax-mp ⊢ Fun ⁡ F
16 vex ⊢ t ∈ V
17 16 funimaex ⊢ Fun ⁡ F → F t ∈ V
18 15 17 ax-mp ⊢ F t ∈ V
19 1 5 6 onvf1odlem2 ⊢ φ → F t ∈ V → C ∈ R1 ⁡ B ∖ F t
20 18 19 mpi ⊢ φ → C ∈ R1 ⁡ B ∖ F t
21 20 eldifad ⊢ φ → C ∈ R1 ⁡ B
22 21 adantr ⊢ φ ∧ t ∈ On → C ∈ R1 ⁡ B
23 13 22 eqeltrd ⊢ φ ∧ t ∈ On → F ⁡ t ∈ R1 ⁡ B
24 rankr1ai ⊢ F ⁡ t ∈ R1 ⁡ B → rank ⁡ F ⁡ t ∈ B
25 onvf1odlem1 ⊢ F t ∈ V → ∃ u ∈ On ∃ v ∈ R1 ⁡ u ¬ v ∈ F t
26 18 25 ax-mp ⊢ ∃ u ∈ On ∃ v ∈ R1 ⁡ u ¬ v ∈ F t
27 onintrab2 ⊢ ∃ u ∈ On ∃ v ∈ R1 ⁡ u ¬ v ∈ F t ↔ ⋂ u ∈ On | ∃ v ∈ R1 ⁡ u ¬ v ∈ F t ∈ On
28 5 eleq1i ⊢ B ∈ On ↔ ⋂ u ∈ On | ∃ v ∈ R1 ⁡ u ¬ v ∈ F t ∈ On
29 27 28 bitr4i ⊢ ∃ u ∈ On ∃ v ∈ R1 ⁡ u ¬ v ∈ F t ↔ B ∈ On
30 26 29 mpbi ⊢ B ∈ On
31 30 oneli ⊢ rank ⁡ F ⁡ t ∈ B → rank ⁡ F ⁡ t ∈ On
32 fveq2 ⊢ u = rank ⁡ F ⁡ t → R1 ⁡ u = R1 ⁡ rank ⁡ F ⁡ t
33 32 rexeqdv ⊢ u = rank ⁡ F ⁡ t → ∃ v ∈ R1 ⁡ u ¬ v ∈ F t ↔ ∃ v ∈ R1 ⁡ rank ⁡ F ⁡ t ¬ v ∈ F t
34 33 onnminsb ⊢ rank ⁡ F ⁡ t ∈ On → rank ⁡ F ⁡ t ∈ ⋂ u ∈ On | ∃ v ∈ R1 ⁡ u ¬ v ∈ F t → ¬ ∃ v ∈ R1 ⁡ rank ⁡ F ⁡ t ¬ v ∈ F t
35 5 eleq2i ⊢ rank ⁡ F ⁡ t ∈ B ↔ rank ⁡ F ⁡ t ∈ ⋂ u ∈ On | ∃ v ∈ R1 ⁡ u ¬ v ∈ F t
36 dfral2 ⊢ ∀ v ∈ R1 ⁡ rank ⁡ F ⁡ t v ∈ F t ↔ ¬ ∃ v ∈ R1 ⁡ rank ⁡ F ⁡ t ¬ v ∈ F t
37 34 35 36 3imtr4g ⊢ rank ⁡ F ⁡ t ∈ On → rank ⁡ F ⁡ t ∈ B → ∀ v ∈ R1 ⁡ rank ⁡ F ⁡ t v ∈ F t
38 31 37 mpcom ⊢ rank ⁡ F ⁡ t ∈ B → ∀ v ∈ R1 ⁡ rank ⁡ F ⁡ t v ∈ F t
39 imassrn ⊢ F t ⊆ ran ⁡ F
40 39 sseli ⊢ v ∈ F t → v ∈ ran ⁡ F
41 40 ralimi ⊢ ∀ v ∈ R1 ⁡ rank ⁡ F ⁡ t v ∈ F t → ∀ v ∈ R1 ⁡ rank ⁡ F ⁡ t v ∈ ran ⁡ F
42 38 41 syl ⊢ rank ⁡ F ⁡ t ∈ B → ∀ v ∈ R1 ⁡ rank ⁡ F ⁡ t v ∈ ran ⁡ F
43 23 24 42 3syl ⊢ φ ∧ t ∈ On → ∀ v ∈ R1 ⁡ rank ⁡ F ⁡ t v ∈ ran ⁡ F
44 2fveq3 ⊢ F ⁡ t = s → R1 ⁡ rank ⁡ F ⁡ t = R1 ⁡ rank ⁡ s
45 44 raleqdv ⊢ F ⁡ t = s → ∀ v ∈ R1 ⁡ rank ⁡ F ⁡ t v ∈ ran ⁡ F ↔ ∀ v ∈ R1 ⁡ rank ⁡ s v ∈ ran ⁡ F
46 43 45 syl5ibcom ⊢ φ ∧ t ∈ On → F ⁡ t = s → ∀ v ∈ R1 ⁡ rank ⁡ s v ∈ ran ⁡ F
47 46 rexlimdva ⊢ φ → ∃ t ∈ On F ⁡ t = s → ∀ v ∈ R1 ⁡ rank ⁡ s v ∈ ran ⁡ F
48 11 47 biimtrid ⊢ φ → s ∈ ran ⁡ F → ∀ v ∈ R1 ⁡ rank ⁡ s v ∈ ran ⁡ F
49 48 imp ⊢ φ ∧ s ∈ ran ⁡ F → ∀ v ∈ R1 ⁡ rank ⁡ s v ∈ ran ⁡ F
50 df-ral ⊢ ∀ v ∈ R1 ⁡ rank ⁡ s v ∈ ran ⁡ F ↔ ∀ v v ∈ R1 ⁡ rank ⁡ s → v ∈ ran ⁡ F
51 49 50 sylib ⊢ φ ∧ s ∈ ran ⁡ F → ∀ v v ∈ R1 ⁡ rank ⁡ s → v ∈ ran ⁡ F
52 51 19.21bi ⊢ φ ∧ s ∈ ran ⁡ F → v ∈ R1 ⁡ rank ⁡ s → v ∈ ran ⁡ F
53 52 con3d ⊢ φ ∧ s ∈ ran ⁡ F → ¬ v ∈ ran ⁡ F → ¬ v ∈ R1 ⁡ rank ⁡ s
54 rankon ⊢ rank ⁡ s ∈ On
55 vex ⊢ v ∈ V
56 55 ssrankr1 ⊢ rank ⁡ s ∈ On → rank ⁡ s ⊆ rank ⁡ v ↔ ¬ v ∈ R1 ⁡ rank ⁡ s
57 54 56 ax-mp ⊢ rank ⁡ s ⊆ rank ⁡ v ↔ ¬ v ∈ R1 ⁡ rank ⁡ s
58 53 57 imbitrrdi ⊢ φ ∧ s ∈ ran ⁡ F → ¬ v ∈ ran ⁡ F → rank ⁡ s ⊆ rank ⁡ v
59 58 impancom ⊢ φ ∧ ¬ v ∈ ran ⁡ F → s ∈ ran ⁡ F → rank ⁡ s ⊆ rank ⁡ v
60 59 ralrimiv ⊢ φ ∧ ¬ v ∈ ran ⁡ F → ∀ s ∈ ran ⁡ F rank ⁡ s ⊆ rank ⁡ v
61 rankon ⊢ rank ⁡ v ∈ On
62 sseq2 ⊢ r = rank ⁡ v → rank ⁡ s ⊆ r ↔ rank ⁡ s ⊆ rank ⁡ v
63 62 ralbidv ⊢ r = rank ⁡ v → ∀ s ∈ ran ⁡ F rank ⁡ s ⊆ r ↔ ∀ s ∈ ran ⁡ F rank ⁡ s ⊆ rank ⁡ v
64 63 rspcev ⊢ rank ⁡ v ∈ On ∧ ∀ s ∈ ran ⁡ F rank ⁡ s ⊆ rank ⁡ v → ∃ r ∈ On ∀ s ∈ ran ⁡ F rank ⁡ s ⊆ r
65 61 64 mpan ⊢ ∀ s ∈ ran ⁡ F rank ⁡ s ⊆ rank ⁡ v → ∃ r ∈ On ∀ s ∈ ran ⁡ F rank ⁡ s ⊆ r
66 bndrank ⊢ ∃ r ∈ On ∀ s ∈ ran ⁡ F rank ⁡ s ⊆ r → ran ⁡ F ∈ V
67 60 65 66 3syl ⊢ φ ∧ ¬ v ∈ ran ⁡ F → ran ⁡ F ∈ V
68 67 expcom ⊢ ¬ v ∈ ran ⁡ F → φ → ran ⁡ F ∈ V
69 68 exlimiv ⊢ ∃ v ¬ v ∈ ran ⁡ F → φ → ran ⁡ F ∈ V
70 8 69 sylbir ⊢ ¬ ∀ v v ∈ ran ⁡ F → φ → ran ⁡ F ∈ V
71 7 70 sylnbi ⊢ ¬ ran ⁡ F = V → φ → ran ⁡ F ∈ V
72 71 com12 ⊢ φ → ¬ ran ⁡ F = V → ran ⁡ F ∈ V
73 72 con1d ⊢ φ → ¬ ran ⁡ F ∈ V → ran ⁡ F = V