Theorem opfi1uzind

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 orderd 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	opfi1uzind.e	⊢ 𝐸 ∈ V
	opfi1uzind.f	⊢ 𝐹 ∈ V
	opfi1uzind.l	⊢ 𝐿 ∈ ℕ0
	opfi1uzind.1	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) )
	opfi1uzind.2	⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) )
	opfi1uzind.3	⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ 𝑛 ∈ 𝑣 ) → ⟨ ( 𝑣 ∖ { 𝑛 } ) , 𝐹 ⟩ ∈ 𝐺 )
	opfi1uzind.4	⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) )
	opfi1uzind.base	⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = 𝐿 ) → 𝜓 )
	opfi1uzind.step	⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 )
Assertion	opfi1uzind	⊢ ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ ( ♯ ‘ 𝑉 ) ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		opfi1uzind.e	⊢ 𝐸 ∈ V
2		opfi1uzind.f	⊢ 𝐹 ∈ V
3		opfi1uzind.l	⊢ 𝐿 ∈ ℕ0
4		opfi1uzind.1	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) )
5		opfi1uzind.2	⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) )
6		opfi1uzind.3	⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ 𝑛 ∈ 𝑣 ) → ⟨ ( 𝑣 ∖ { 𝑛 } ) , 𝐹 ⟩ ∈ 𝐺 )
7		opfi1uzind.4	⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) )
8		opfi1uzind.base	⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = 𝐿 ) → 𝜓 )
9		opfi1uzind.step	⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 )
10	1	a1i	⊢ ( 𝑎 = 𝑉 → 𝐸 ∈ V )
11		opeq12	⊢ ( ( 𝑎 = 𝑉 ∧ 𝑏 = 𝐸 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑉 , 𝐸 ⟩ )
12	11	eleq1d	⊢ ( ( 𝑎 = 𝑉 ∧ 𝑏 = 𝐸 ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ↔ ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ) )
13	10 12	sbcied	⊢ ( 𝑎 = 𝑉 → ( [ 𝐸 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ↔ ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ) )
14	13	sbcieg	⊢ ( 𝑉 ∈ Fin → ( [ 𝑉 / 𝑎 ] [ 𝐸 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ↔ ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ) )
15	14	biimparc	⊢ ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ) → [ 𝑉 / 𝑎 ] [ 𝐸 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 )
16	15	3adant3	⊢ ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ ( ♯ ‘ 𝑉 ) ) → [ 𝑉 / 𝑎 ] [ 𝐸 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 )
17		vex	⊢ 𝑣 ∈ V
18		vex	⊢ 𝑒 ∈ V
19		opeq12	⊢ ( ( 𝑎 = 𝑣 ∧ 𝑏 = 𝑒 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑣 , 𝑒 ⟩ )
20	19	eleq1d	⊢ ( ( 𝑎 = 𝑣 ∧ 𝑏 = 𝑒 ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ↔ ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ) )
21	17 18 20	sbc2ie	⊢ ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ↔ ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 )
22	21 6	sylanb	⊢ ( ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ∧ 𝑛 ∈ 𝑣 ) → ⟨ ( 𝑣 ∖ { 𝑛 } ) , 𝐹 ⟩ ∈ 𝐺 )
23	17	difexi	⊢ ( 𝑣 ∖ { 𝑛 } ) ∈ V
24		opeq12	⊢ ( ( 𝑎 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑏 = 𝐹 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( 𝑣 ∖ { 𝑛 } ) , 𝐹 ⟩ )
25	24	eleq1d	⊢ ( ( 𝑎 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑏 = 𝐹 ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ↔ ⟨ ( 𝑣 ∖ { 𝑛 } ) , 𝐹 ⟩ ∈ 𝐺 ) )
26	23 2 25	sbc2ie	⊢ ( [ ( 𝑣 ∖ { 𝑛 } ) / 𝑎 ] [ 𝐹 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ↔ ⟨ ( 𝑣 ∖ { 𝑛 } ) , 𝐹 ⟩ ∈ 𝐺 )
27	22 26	sylibr	⊢ ( ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ∧ 𝑛 ∈ 𝑣 ) → [ ( 𝑣 ∖ { 𝑛 } ) / 𝑎 ] [ 𝐹 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 )
28	21 8	sylanb	⊢ ( ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = 𝐿 ) → 𝜓 )
29	21	3anbi1i	⊢ ( ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ↔ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) )
30	29	anbi2i	⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ↔ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) )
31	30 9	sylanb	⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 )
32	2 3 4 5 27 7 28 31	fi1uzind	⊢ ( ( [ 𝑉 / 𝑎 ] [ 𝐸 / 𝑏 ] ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ ( ♯ ‘ 𝑉 ) ) → 𝜑 )
33	16 32	syld3an1	⊢ ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ ( ♯ ‘ 𝑉 ) ) → 𝜑 )