Metamath Proof Explorer

Theorem fi1uzind

Description: Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as ordered pairs of vertices and edges) with a finite number of vertices, usually with L = 0 (see opfi1ind ) or L = 1 . (Contributed by AV, 22-Oct-2020) (Revised by AV, 28-Mar-2021)

Ref Expression
Hypotheses fi1uzind.f ⊢ F ∈ V
fi1uzind.l ⊢ L ∈ ℕ 0
fi1uzind.1 ⊢ v = V ∧ e = E → ψ ↔ φ
fi1uzind.2 ⊢ v = w ∧ e = f → ψ ↔ θ
fi1uzind.3 ⊢ [˙v / a]˙ [˙e / b]˙ ρ ∧ n ∈ v → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ
fi1uzind.4 ⊢ w = v ∖ n ∧ f = F → θ ↔ χ
fi1uzind.base ⊢ [˙v / a]˙ [˙e / b]˙ ρ ∧ v = L → ψ
fi1uzind.step ⊢ y + 1 ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ v = y + 1 ∧ n ∈ v ∧ χ → ψ
Assertion fi1uzind ⊢ [˙V / a]˙ [˙E / b]˙ ρ ∧ V ∈ Fin ∧ L ≤ V → φ

Proof

Step Hyp Ref Expression
1 fi1uzind.f ⊢ F ∈ V
2 fi1uzind.l ⊢ L ∈ ℕ 0
3 fi1uzind.1 ⊢ v = V ∧ e = E → ψ ↔ φ
4 fi1uzind.2 ⊢ v = w ∧ e = f → ψ ↔ θ
5 fi1uzind.3 ⊢ [˙v / a]˙ [˙e / b]˙ ρ ∧ n ∈ v → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ
6 fi1uzind.4 ⊢ w = v ∖ n ∧ f = F → θ ↔ χ
7 fi1uzind.base ⊢ [˙v / a]˙ [˙e / b]˙ ρ ∧ v = L → ψ
8 fi1uzind.step ⊢ y + 1 ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ v = y + 1 ∧ n ∈ v ∧ χ → ψ
9 dfclel ⊢ V ∈ ℕ 0 ↔ ∃ n n = V ∧ n ∈ ℕ 0
10 nn0z ⊢ L ∈ ℕ 0 → L ∈ ℤ
11 2 10 mp1i ⊢ L ≤ V ∧ n ∈ ℕ 0 ∧ n = V → L ∈ ℤ
12 nn0z ⊢ n ∈ ℕ 0 → n ∈ ℤ
13 12 ad2antlr ⊢ L ≤ V ∧ n ∈ ℕ 0 ∧ n = V → n ∈ ℤ
14 breq2 ⊢ V = n → L ≤ V ↔ L ≤ n
15 14 eqcoms ⊢ n = V → L ≤ V ↔ L ≤ n
16 15 biimpcd ⊢ L ≤ V → n = V → L ≤ n
17 16 adantr ⊢ L ≤ V ∧ n ∈ ℕ 0 → n = V → L ≤ n
18 17 imp ⊢ L ≤ V ∧ n ∈ ℕ 0 ∧ n = V → L ≤ n
19 eqeq1 ⊢ x = L → x = v ↔ L = v
20 19 anbi2d ⊢ x = L → [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v ↔ [˙v / a]˙ [˙e / b]˙ ρ ∧ L = v
21 20 imbi1d ⊢ x = L → [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v → ψ ↔ [˙v / a]˙ [˙e / b]˙ ρ ∧ L = v → ψ
22 21 2albidv ⊢ x = L → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v → ψ ↔ ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ L = v → ψ
23 eqeq1 ⊢ x = y → x = v ↔ y = v
24 23 anbi2d ⊢ x = y → [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v ↔ [˙v / a]˙ [˙e / b]˙ ρ ∧ y = v
25 24 imbi1d ⊢ x = y → [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v → ψ ↔ [˙v / a]˙ [˙e / b]˙ ρ ∧ y = v → ψ
26 25 2albidv ⊢ x = y → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v → ψ ↔ ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ y = v → ψ
27 eqeq1 ⊢ x = y + 1 → x = v ↔ y + 1 = v
28 27 anbi2d ⊢ x = y + 1 → [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v ↔ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v
29 28 imbi1d ⊢ x = y + 1 → [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v → ψ ↔ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → ψ
30 29 2albidv ⊢ x = y + 1 → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v → ψ ↔ ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → ψ
31 eqeq1 ⊢ x = n → x = v ↔ n = v
32 31 anbi2d ⊢ x = n → [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v ↔ [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v
33 32 imbi1d ⊢ x = n → [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v → ψ ↔ [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ
34 33 2albidv ⊢ x = n → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ x = v → ψ ↔ ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ
35 eqcom ⊢ L = v ↔ v = L
36 35 7 sylan2b ⊢ [˙v / a]˙ [˙e / b]˙ ρ ∧ L = v → ψ
37 36 gen2 ⊢ ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ L = v → ψ
38 37 a1i ⊢ L ∈ ℤ → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ L = v → ψ
39 simpl ⊢ v = w ∧ e = f → v = w
40 simpr ⊢ v = w ∧ e = f → e = f
41 40 sbceq1d ⊢ v = w ∧ e = f → [˙e / b]˙ ρ ↔ [˙f / b]˙ ρ
42 39 41 sbceqbid ⊢ v = w ∧ e = f → [˙v / a]˙ [˙e / b]˙ ρ ↔ [˙w / a]˙ [˙f / b]˙ ρ
43 fveq2 ⊢ v = w → v = w
44 43 eqeq2d ⊢ v = w → y = v ↔ y = w
45 44 adantr ⊢ v = w ∧ e = f → y = v ↔ y = w
46 42 45 anbi12d ⊢ v = w ∧ e = f → [˙v / a]˙ [˙e / b]˙ ρ ∧ y = v ↔ [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w
47 46 4 imbi12d ⊢ v = w ∧ e = f → [˙v / a]˙ [˙e / b]˙ ρ ∧ y = v → ψ ↔ [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ
48 47 cbval2vw ⊢ ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ y = v → ψ ↔ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ
49 nn0ge0 ⊢ L ∈ ℕ 0 → 0 ≤ L
50 0red ⊢ y ∈ ℤ → 0 ∈ ℝ
51 nn0re ⊢ L ∈ ℕ 0 → L ∈ ℝ
52 2 51 mp1i ⊢ y ∈ ℤ → L ∈ ℝ
53 zre ⊢ y ∈ ℤ → y ∈ ℝ
54 letr ⊢ 0 ∈ ℝ ∧ L ∈ ℝ ∧ y ∈ ℝ → 0 ≤ L ∧ L ≤ y → 0 ≤ y
55 50 52 53 54 syl3anc ⊢ y ∈ ℤ → 0 ≤ L ∧ L ≤ y → 0 ≤ y
56 0nn0 ⊢ 0 ∈ ℕ 0
57 pm3.22 ⊢ 0 ≤ y ∧ y ∈ ℤ → y ∈ ℤ ∧ 0 ≤ y
58 0z ⊢ 0 ∈ ℤ
59 eluz1 ⊢ 0 ∈ ℤ → y ∈ ℤ ≥ 0 ↔ y ∈ ℤ ∧ 0 ≤ y
60 58 59 mp1i ⊢ 0 ≤ y ∧ y ∈ ℤ → y ∈ ℤ ≥ 0 ↔ y ∈ ℤ ∧ 0 ≤ y
61 57 60 mpbird ⊢ 0 ≤ y ∧ y ∈ ℤ → y ∈ ℤ ≥ 0
62 eluznn0 ⊢ 0 ∈ ℕ 0 ∧ y ∈ ℤ ≥ 0 → y ∈ ℕ 0
63 56 61 62 sylancr ⊢ 0 ≤ y ∧ y ∈ ℤ → y ∈ ℕ 0
64 63 ex ⊢ 0 ≤ y → y ∈ ℤ → y ∈ ℕ 0
65 55 64 syl6com ⊢ 0 ≤ L ∧ L ≤ y → y ∈ ℤ → y ∈ ℤ → y ∈ ℕ 0
66 65 ex ⊢ 0 ≤ L → L ≤ y → y ∈ ℤ → y ∈ ℤ → y ∈ ℕ 0
67 66 com14 ⊢ y ∈ ℤ → L ≤ y → y ∈ ℤ → 0 ≤ L → y ∈ ℕ 0
68 67 pm2.43a ⊢ y ∈ ℤ → L ≤ y → 0 ≤ L → y ∈ ℕ 0
69 68 imp ⊢ y ∈ ℤ ∧ L ≤ y → 0 ≤ L → y ∈ ℕ 0
70 69 com12 ⊢ 0 ≤ L → y ∈ ℤ ∧ L ≤ y → y ∈ ℕ 0
71 2 49 70 mp2b ⊢ y ∈ ℤ ∧ L ≤ y → y ∈ ℕ 0
72 71 3adant1 ⊢ L ∈ ℤ ∧ y ∈ ℤ ∧ L ≤ y → y ∈ ℕ 0
73 eqcom ⊢ y + 1 = v ↔ v = y + 1
74 nn0p1gt0 ⊢ y ∈ ℕ 0 → 0 < y + 1
75 74 adantr ⊢ y ∈ ℕ 0 ∧ v = y + 1 → 0 < y + 1
76 simpr ⊢ y ∈ ℕ 0 ∧ v = y + 1 → v = y + 1
77 75 76 breqtrrd ⊢ y ∈ ℕ 0 ∧ v = y + 1 → 0 < v
78 73 77 sylan2b ⊢ y ∈ ℕ 0 ∧ y + 1 = v → 0 < v
79 78 adantrl ⊢ y ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → 0 < v
80 hashgt0elex ⊢ v ∈ V ∧ 0 < v → ∃ n n ∈ v
81 vex ⊢ v ∈ V
82 81 a1i ⊢ y ∈ ℕ 0 ∧ n ∈ v → v ∈ V
83 simpr ⊢ y ∈ ℕ 0 ∧ n ∈ v → n ∈ v
84 simpl ⊢ y ∈ ℕ 0 ∧ n ∈ v → y ∈ ℕ 0
85 hashdifsnp1 ⊢ v ∈ V ∧ n ∈ v ∧ y ∈ ℕ 0 → v = y + 1 → v ∖ n = y
86 73 85 biimtrid ⊢ v ∈ V ∧ n ∈ v ∧ y ∈ ℕ 0 → y + 1 = v → v ∖ n = y
87 82 83 84 86 syl3anc ⊢ y ∈ ℕ 0 ∧ n ∈ v → y + 1 = v → v ∖ n = y
88 87 imp ⊢ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v → v ∖ n = y
89 peano2nn0 ⊢ y ∈ ℕ 0 → y + 1 ∈ ℕ 0
90 89 ad2antrr ⊢ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v → y + 1 ∈ ℕ 0
91 90 ad2antlr ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v ∧ [˙v / a]˙ [˙e / b]˙ ρ → y + 1 ∈ ℕ 0
92 simpr ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v ∧ [˙v / a]˙ [˙e / b]˙ ρ → [˙v / a]˙ [˙e / b]˙ ρ
93 simplrr ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v ∧ [˙v / a]˙ [˙e / b]˙ ρ → y + 1 = v
94 simprlr ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v → n ∈ v
95 94 adantr ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v ∧ [˙v / a]˙ [˙e / b]˙ ρ → n ∈ v
96 92 93 95 3jca ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v ∧ [˙v / a]˙ [˙e / b]˙ ρ → [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v ∧ n ∈ v
97 91 96 jca ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v ∧ [˙v / a]˙ [˙e / b]˙ ρ → y + 1 ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v ∧ n ∈ v
98 81 difexi ⊢ v ∖ n ∈ V
99 simpl ⊢ w = v ∖ n ∧ f = F → w = v ∖ n
100 simpr ⊢ w = v ∖ n ∧ f = F → f = F
101 100 sbceq1d ⊢ w = v ∖ n ∧ f = F → [˙f / b]˙ ρ ↔ [˙F / b]˙ ρ
102 99 101 sbceqbid ⊢ w = v ∖ n ∧ f = F → [˙w / a]˙ [˙f / b]˙ ρ ↔ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ
103 eqcom ⊢ y = w ↔ w = y
104 fveqeq2 ⊢ w = v ∖ n → w = y ↔ v ∖ n = y
105 103 104 bitrid ⊢ w = v ∖ n → y = w ↔ v ∖ n = y
106 105 adantr ⊢ w = v ∖ n ∧ f = F → y = w ↔ v ∖ n = y
107 102 106 anbi12d ⊢ w = v ∖ n ∧ f = F → [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w ↔ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ v ∖ n = y
108 107 6 imbi12d ⊢ w = v ∖ n ∧ f = F → [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ↔ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ v ∖ n = y → χ
109 108 spc2gv ⊢ v ∖ n ∈ V ∧ F ∈ V → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ v ∖ n = y → χ
110 98 1 109 mp2an ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ v ∖ n = y → χ
111 110 expdimp ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → v ∖ n = y → χ
112 111 ad2antrr ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v ∧ [˙v / a]˙ [˙e / b]˙ ρ → v ∖ n = y → χ
113 73 3anbi2i ⊢ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v ∧ n ∈ v ↔ [˙v / a]˙ [˙e / b]˙ ρ ∧ v = y + 1 ∧ n ∈ v
114 113 anbi2i ⊢ y + 1 ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v ∧ n ∈ v ↔ y + 1 ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ v = y + 1 ∧ n ∈ v
115 114 8 sylanb ⊢ y + 1 ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v ∧ n ∈ v ∧ χ → ψ
116 97 112 115 syl6an ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ ∧ [˙ v ∖ n / a]˙ [˙F / b]˙ ρ ∧ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v ∧ [˙v / a]˙ [˙e / b]˙ ρ → v ∖ n = y → ψ
117 116 exp41 ⊢ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v → [˙v / a]˙ [˙e / b]˙ ρ → v ∖ n = y → ψ
118 117 com15 ⊢ v ∖ n = y → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
119 118 com23 ⊢ v ∖ n = y → y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
120 88 119 mpcom ⊢ y ∈ ℕ 0 ∧ n ∈ v ∧ y + 1 = v → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
121 120 ex ⊢ y ∈ ℕ 0 ∧ n ∈ v → y + 1 = v → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
122 121 com23 ⊢ y ∈ ℕ 0 ∧ n ∈ v → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → y + 1 = v → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
123 122 ex ⊢ y ∈ ℕ 0 → n ∈ v → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → y + 1 = v → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
124 123 com15 ⊢ [˙v / a]˙ [˙e / b]˙ ρ → n ∈ v → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → y + 1 = v → y ∈ ℕ 0 → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
125 124 imp ⊢ [˙v / a]˙ [˙e / b]˙ ρ ∧ n ∈ v → [˙ v ∖ n / a]˙ [˙F / b]˙ ρ → y + 1 = v → y ∈ ℕ 0 → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
126 5 125 mpd ⊢ [˙v / a]˙ [˙e / b]˙ ρ ∧ n ∈ v → y + 1 = v → y ∈ ℕ 0 → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
127 126 ex ⊢ [˙v / a]˙ [˙e / b]˙ ρ → n ∈ v → y + 1 = v → y ∈ ℕ 0 → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
128 127 com4l ⊢ n ∈ v → y + 1 = v → y ∈ ℕ 0 → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
129 128 exlimiv ⊢ ∃ n n ∈ v → y + 1 = v → y ∈ ℕ 0 → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
130 80 129 syl ⊢ v ∈ V ∧ 0 < v → y + 1 = v → y ∈ ℕ 0 → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
131 130 ex ⊢ v ∈ V → 0 < v → y + 1 = v → y ∈ ℕ 0 → [˙v / a]˙ [˙e / b]˙ ρ → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
132 131 com25 ⊢ v ∈ V → [˙v / a]˙ [˙e / b]˙ ρ → y + 1 = v → y ∈ ℕ 0 → 0 < v → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
133 132 elv ⊢ [˙v / a]˙ [˙e / b]˙ ρ → y + 1 = v → y ∈ ℕ 0 → 0 < v → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
134 133 imp ⊢ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → y ∈ ℕ 0 → 0 < v → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
135 134 impcom ⊢ y ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → 0 < v → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
136 79 135 mpd ⊢ y ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
137 72 136 sylan ⊢ L ∈ ℤ ∧ y ∈ ℤ ∧ L ≤ y ∧ [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ψ
138 137 impancom ⊢ L ∈ ℤ ∧ y ∈ ℤ ∧ L ≤ y ∧ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → ψ
139 138 alrimivv ⊢ L ∈ ℤ ∧ y ∈ ℤ ∧ L ≤ y ∧ ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → ψ
140 139 ex ⊢ L ∈ ℤ ∧ y ∈ ℤ ∧ L ≤ y → ∀ w ∀ f [˙w / a]˙ [˙f / b]˙ ρ ∧ y = w → θ → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → ψ
141 48 140 biimtrid ⊢ L ∈ ℤ ∧ y ∈ ℤ ∧ L ≤ y → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ y = v → ψ → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ y + 1 = v → ψ
142 22 26 30 34 38 141 uzind ⊢ L ∈ ℤ ∧ n ∈ ℤ ∧ L ≤ n → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ
143 11 13 18 142 syl3anc ⊢ L ≤ V ∧ n ∈ ℕ 0 ∧ n = V → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ
144 sbcex ⊢ [˙V / a]˙ [˙E / b]˙ ρ → V ∈ V
145 sbccom ⊢ [˙V / a]˙ [˙E / b]˙ ρ ↔ [˙E / b]˙ [˙V / a]˙ ρ
146 sbcex ⊢ [˙E / b]˙ [˙V / a]˙ ρ → E ∈ V
147 145 146 sylbi ⊢ [˙V / a]˙ [˙E / b]˙ ρ → E ∈ V
148 144 147 jca ⊢ [˙V / a]˙ [˙E / b]˙ ρ → V ∈ V ∧ E ∈ V
149 simpl ⊢ v = V ∧ e = E → v = V
150 simpr ⊢ v = V ∧ e = E → e = E
151 150 sbceq1d ⊢ v = V ∧ e = E → [˙e / b]˙ ρ ↔ [˙E / b]˙ ρ
152 149 151 sbceqbid ⊢ v = V ∧ e = E → [˙v / a]˙ [˙e / b]˙ ρ ↔ [˙V / a]˙ [˙E / b]˙ ρ
153 fveq2 ⊢ v = V → v = V
154 153 eqeq2d ⊢ v = V → n = v ↔ n = V
155 154 adantr ⊢ v = V ∧ e = E → n = v ↔ n = V
156 152 155 anbi12d ⊢ v = V ∧ e = E → [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v ↔ [˙V / a]˙ [˙E / b]˙ ρ ∧ n = V
157 156 3 imbi12d ⊢ v = V ∧ e = E → [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ ↔ [˙V / a]˙ [˙E / b]˙ ρ ∧ n = V → φ
158 157 spc2gv ⊢ V ∈ V ∧ E ∈ V → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ → [˙V / a]˙ [˙E / b]˙ ρ ∧ n = V → φ
159 158 com23 ⊢ V ∈ V ∧ E ∈ V → [˙V / a]˙ [˙E / b]˙ ρ ∧ n = V → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ → φ
160 159 expd ⊢ V ∈ V ∧ E ∈ V → [˙V / a]˙ [˙E / b]˙ ρ → n = V → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ → φ
161 148 160 mpcom ⊢ [˙V / a]˙ [˙E / b]˙ ρ → n = V → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ → φ
162 161 imp ⊢ [˙V / a]˙ [˙E / b]˙ ρ ∧ n = V → ∀ v ∀ e [˙v / a]˙ [˙e / b]˙ ρ ∧ n = v → ψ → φ
163 143 162 syl5com ⊢ L ≤ V ∧ n ∈ ℕ 0 ∧ n = V → [˙V / a]˙ [˙E / b]˙ ρ ∧ n = V → φ
164 163 exp31 ⊢ L ≤ V → n ∈ ℕ 0 → n = V → [˙V / a]˙ [˙E / b]˙ ρ ∧ n = V → φ
165 164 com14 ⊢ [˙V / a]˙ [˙E / b]˙ ρ ∧ n = V → n ∈ ℕ 0 → n = V → L ≤ V → φ
166 165 expcom ⊢ n = V → [˙V / a]˙ [˙E / b]˙ ρ → n ∈ ℕ 0 → n = V → L ≤ V → φ
167 166 com24 ⊢ n = V → n = V → n ∈ ℕ 0 → [˙V / a]˙ [˙E / b]˙ ρ → L ≤ V → φ
168 167 pm2.43i ⊢ n = V → n ∈ ℕ 0 → [˙V / a]˙ [˙E / b]˙ ρ → L ≤ V → φ
169 168 imp ⊢ n = V ∧ n ∈ ℕ 0 → [˙V / a]˙ [˙E / b]˙ ρ → L ≤ V → φ
170 169 exlimiv ⊢ ∃ n n = V ∧ n ∈ ℕ 0 → [˙V / a]˙ [˙E / b]˙ ρ → L ≤ V → φ
171 9 170 sylbi ⊢ V ∈ ℕ 0 → [˙V / a]˙ [˙E / b]˙ ρ → L ≤ V → φ
172 hashcl ⊢ V ∈ Fin → V ∈ ℕ 0
173 171 172 syl11 ⊢ [˙V / a]˙ [˙E / b]˙ ρ → V ∈ Fin → L ≤ V → φ
174 173 3imp ⊢ [˙V / a]˙ [˙E / b]˙ ρ ∧ V ∈ Fin ∧ L ≤ V → φ