Theorem fncnv

Description: Single-rootedness (see funcnv ) of a class cut down by a Cartesian product. (Contributed by NM, 5-Mar-2007)

	Ref	Expression
Assertion	fncnv	⊢ ( ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) Fn 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		df-fn	⊢ ( ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) Fn 𝐵 ↔ ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ dom ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) )
2		df-rn	⊢ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = dom ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) )
3	2	eqeq1i	⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ dom ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 )
4	3	anbi2i	⊢ ( ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) ↔ ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ dom ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) )
5		rninxp	⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )
6	5	anbi1i	⊢ ( ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
7		funcnv	⊢ ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑦 ∈ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 )
8		raleq	⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 → ( ∀ 𝑦 ∈ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ) )
9		biimt	⊢ ( 𝑦 ∈ 𝐵 → ( ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ↔ ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) ) )
10		moanimv	⊢ ( ∃* 𝑥 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) ↔ ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
11		brinxp2	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) )
12		an21	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
13	11 12	bitri	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
14	13	mobii	⊢ ( ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∃* 𝑥 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
15		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
16	15	imbi2i	⊢ ( ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) ↔ ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
17	10 14 16	3bitr4i	⊢ ( ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
18	9 17	syl6rbbr	⊢ ( 𝑦 ∈ 𝐵 → ( ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
19	18	ralbiia	⊢ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )
20	8 19	syl6bb	⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 → ( ∀ 𝑦 ∈ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∃* 𝑥 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
21	7 20	syl5bb	⊢ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 → ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
22	21	pm5.32i	⊢ ( ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) ↔ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
23		r19.26	⊢ ( ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
24	6 22 23	3bitr4i	⊢ ( ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
25		ancom	⊢ ( ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) ↔ ( ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ∧ Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) )
26		reu5	⊢ ( ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ↔ ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
27	26	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ∧ ∃* 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ) )
28	24 25 27	3bitr4i	⊢ ( ( Fun ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ ran ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )
29	1 4 28	3bitr2i	⊢ ( ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) Fn 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 )