lfgrnloop

Description: A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Hypotheses	lfuhgrnloopv.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	lfuhgrnloopv.a	⊢ 𝐴 = dom 𝐼
	lfuhgrnloopv.e	⊢ 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
Assertion	lfgrnloop	⊢ ( 𝐼 : 𝐴 ⟶ 𝐸 → { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		lfuhgrnloopv.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		lfuhgrnloopv.a	⊢ 𝐴 = dom 𝐼
3		lfuhgrnloopv.e	⊢ 𝐸 = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
4		nfcv	⊢ Ⅎ 𝑥 𝐼
5		nfcv	⊢ Ⅎ 𝑥 𝐴
6		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
7	3 6	nfcxfr	⊢ Ⅎ 𝑥 𝐸
8	4 5 7	nff	⊢ Ⅎ 𝑥 𝐼 : 𝐴 ⟶ 𝐸
9		hashsn01	⊢ ( ( ♯ ‘ { 𝑈 } ) = 0 ∨ ( ♯ ‘ { 𝑈 } ) = 1 )
10		2pos	⊢ 0 < 2
11		0re	⊢ 0 ∈ ℝ
12		2re	⊢ 2 ∈ ℝ
13	11 12	ltnlei	⊢ ( 0 < 2 ↔ ¬ 2 ≤ 0 )
14	10 13	mpbi	⊢ ¬ 2 ≤ 0
15		breq2	⊢ ( ( ♯ ‘ { 𝑈 } ) = 0 → ( 2 ≤ ( ♯ ‘ { 𝑈 } ) ↔ 2 ≤ 0 ) )
16	14 15	mtbiri	⊢ ( ( ♯ ‘ { 𝑈 } ) = 0 → ¬ 2 ≤ ( ♯ ‘ { 𝑈 } ) )
17		1lt2	⊢ 1 < 2
18		1re	⊢ 1 ∈ ℝ
19	18 12	ltnlei	⊢ ( 1 < 2 ↔ ¬ 2 ≤ 1 )
20	17 19	mpbi	⊢ ¬ 2 ≤ 1
21		breq2	⊢ ( ( ♯ ‘ { 𝑈 } ) = 1 → ( 2 ≤ ( ♯ ‘ { 𝑈 } ) ↔ 2 ≤ 1 ) )
22	20 21	mtbiri	⊢ ( ( ♯ ‘ { 𝑈 } ) = 1 → ¬ 2 ≤ ( ♯ ‘ { 𝑈 } ) )
23	16 22	jaoi	⊢ ( ( ( ♯ ‘ { 𝑈 } ) = 0 ∨ ( ♯ ‘ { 𝑈 } ) = 1 ) → ¬ 2 ≤ ( ♯ ‘ { 𝑈 } ) )
24	9 23	ax-mp	⊢ ¬ 2 ≤ ( ♯ ‘ { 𝑈 } )
25		fveq2	⊢ ( ( 𝐼 ‘ 𝑥 ) = { 𝑈 } → ( ♯ ‘ ( 𝐼 ‘ 𝑥 ) ) = ( ♯ ‘ { 𝑈 } ) )
26	25	breq2d	⊢ ( ( 𝐼 ‘ 𝑥 ) = { 𝑈 } → ( 2 ≤ ( ♯ ‘ ( 𝐼 ‘ 𝑥 ) ) ↔ 2 ≤ ( ♯ ‘ { 𝑈 } ) ) )
27	24 26	mtbiri	⊢ ( ( 𝐼 ‘ 𝑥 ) = { 𝑈 } → ¬ 2 ≤ ( ♯ ‘ ( 𝐼 ‘ 𝑥 ) ) )
28	1 2 3	lfgredgge2	⊢ ( ( 𝐼 : 𝐴 ⟶ 𝐸 ∧ 𝑥 ∈ 𝐴 ) → 2 ≤ ( ♯ ‘ ( 𝐼 ‘ 𝑥 ) ) )
29	27 28	nsyl3	⊢ ( ( 𝐼 : 𝐴 ⟶ 𝐸 ∧ 𝑥 ∈ 𝐴 ) → ¬ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } )
30	29	ex	⊢ ( 𝐼 : 𝐴 ⟶ 𝐸 → ( 𝑥 ∈ 𝐴 → ¬ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } ) )
31	8 30	ralrimi	⊢ ( 𝐼 : 𝐴 ⟶ 𝐸 → ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } )
32		rabeq0	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } )
33	31 32	sylibr	⊢ ( 𝐼 : 𝐴 ⟶ 𝐸 → { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } = ∅ )

Metamath Proof Explorer

Theorem lfgrnloop

Proof