Theorem brfi1uzind

Description: Properties of a binary relation 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 (as binary relation between the set of vertices and an edge function) with a finite number of vertices, usually with L = 0 (see brfi1ind ) or L = 1 . (Contributed by Alexander van der Vekens, 7-Jan-2018) (Proof shortened by AV, 23-Oct-2020) (Revised by AV, 28-Mar-2021)

	Ref	Expression
Hypotheses	brfi1uzind.r	⊢ Rel 𝐺
	brfi1uzind.f	⊢ 𝐹 ∈ V
	brfi1uzind.l	⊢ 𝐿 ∈ ℕ0
	brfi1uzind.1	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) )
	brfi1uzind.2	⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) )
	brfi1uzind.3	⊢ ( ( 𝑣 𝐺 𝑒 ∧ 𝑛 ∈ 𝑣 ) → ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 )
	brfi1uzind.4	⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) )
	brfi1uzind.base	⊢ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝐿 ) → 𝜓 )
	brfi1uzind.step	⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 )
Assertion	brfi1uzind	⊢ ( ( 𝑉 𝐺 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ ( ♯ ‘ 𝑉 ) ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		brfi1uzind.r	⊢ Rel 𝐺
2		brfi1uzind.f	⊢ 𝐹 ∈ V
3		brfi1uzind.l	⊢ 𝐿 ∈ ℕ0
4		brfi1uzind.1	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) )
5		brfi1uzind.2	⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) )
6		brfi1uzind.3	⊢ ( ( 𝑣 𝐺 𝑒 ∧ 𝑛 ∈ 𝑣 ) → ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 )
7		brfi1uzind.4	⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) )
8		brfi1uzind.base	⊢ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 𝐿 ) → 𝜓 )
9		brfi1uzind.step	⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 )
10	1	brrelex12i	⊢ ( 𝑉 𝐺 𝐸 → ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) )
11		simpl	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → 𝑉 ∈ V )
12		simplr	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ 𝑎 = 𝑉 ) → 𝐸 ∈ V )
13		breq12	⊢ ( ( 𝑎 = 𝑉 ∧ 𝑏 = 𝐸 ) → ( 𝑎 𝐺 𝑏 ↔ 𝑉 𝐺 𝐸 ) )
14	13	adantll	⊢ ( ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ 𝑎 = 𝑉 ) ∧ 𝑏 = 𝐸 ) → ( 𝑎 𝐺 𝑏 ↔ 𝑉 𝐺 𝐸 ) )
15	12 14	sbcied	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ 𝑎 = 𝑉 ) → ( [ 𝐸 / 𝑏 ] 𝑎 𝐺 𝑏 ↔ 𝑉 𝐺 𝐸 ) )
16	11 15	sbcied	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( [ 𝑉 / 𝑎 ] [ 𝐸 / 𝑏 ] 𝑎 𝐺 𝑏 ↔ 𝑉 𝐺 𝐸 ) )
17	16	biimprcd	⊢ ( 𝑉 𝐺 𝐸 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → [ 𝑉 / 𝑎 ] [ 𝐸 / 𝑏 ] 𝑎 𝐺 𝑏 ) )
18	10 17	mpd	⊢ ( 𝑉 𝐺 𝐸 → [ 𝑉 / 𝑎 ] [ 𝐸 / 𝑏 ] 𝑎 𝐺 𝑏 )
19		vex	⊢ 𝑣 ∈ V
20		vex	⊢ 𝑒 ∈ V
21		breq12	⊢ ( ( 𝑎 = 𝑣 ∧ 𝑏 = 𝑒 ) → ( 𝑎 𝐺 𝑏 ↔ 𝑣 𝐺 𝑒 ) )
22	19 20 21	sbc2ie	⊢ ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] 𝑎 𝐺 𝑏 ↔ 𝑣 𝐺 𝑒 )
23	19	difexi	⊢ ( 𝑣 ∖ { 𝑛 } ) ∈ V
24		breq12	⊢ ( ( 𝑎 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑏 = 𝐹 ) → ( 𝑎 𝐺 𝑏 ↔ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) )
25	23 2 24	sbc2ie	⊢ ( [ ( 𝑣 ∖ { 𝑛 } ) / 𝑎 ] [ 𝐹 / 𝑏 ] 𝑎 𝐺 𝑏 ↔ ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 )
26	6 25	sylibr	⊢ ( ( 𝑣 𝐺 𝑒 ∧ 𝑛 ∈ 𝑣 ) → [ ( 𝑣 ∖ { 𝑛 } ) / 𝑎 ] [ 𝐹 / 𝑏 ] 𝑎 𝐺 𝑏 )
27	22 26	sylanb	⊢ ( ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] 𝑎 𝐺 𝑏 ∧ 𝑛 ∈ 𝑣 ) → [ ( 𝑣 ∖ { 𝑛 } ) / 𝑎 ] [ 𝐹 / 𝑏 ] 𝑎 𝐺 𝑏 )
28	22 8	sylanb	⊢ ( ( [ 𝑣 / 𝑎 ] [ 𝑒 / 𝑏 ] 𝑎 𝐺 𝑏 ∧ ( ♯ ‘ 𝑣 ) = 𝐿 ) → 𝜓 )
29	22	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	18 32	syl3an1	⊢ ( ( 𝑉 𝐺 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ ( ♯ ‘ 𝑉 ) ) → 𝜑 )