This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oacomf1olem

Description: Lemma for oacomf1o . (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypothesis oacomf1olem.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 +o 𝑥 ) )
Assertion oacomf1olem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ∧ ( ran 𝐹 ∩ 𝐵 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 oacomf1olem.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 +o 𝑥 ) )
2 oaf1o ⊢ ( 𝐵 ∈ On → ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) : On –1-1-onto→ ( On ∖ 𝐵 ) )
3 2 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) : On –1-1-onto→ ( On ∖ 𝐵 ) )
4 f1of1 ⊢ ( ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) : On –1-1-onto→ ( On ∖ 𝐵 ) → ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) : On –1-1→ ( On ∖ 𝐵 ) )
5 3 4 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) : On –1-1→ ( On ∖ 𝐵 ) )
6 onss ⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
7 6 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ On )
8 f1ssres ⊢ ( ( ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) : On –1-1→ ( On ∖ 𝐵 ) ∧ 𝐴 ⊆ On ) → ( ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) ↾ 𝐴 ) : 𝐴 –1-1→ ( On ∖ 𝐵 ) )
9 5 7 8 syl2anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) ↾ 𝐴 ) : 𝐴 –1-1→ ( On ∖ 𝐵 ) )
10 7 resmptd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 +o 𝑥 ) ) )
11 10 1 eqtr4di ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) ↾ 𝐴 ) = 𝐹 )
12 f1eq1 ⊢ ( ( ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) ↾ 𝐴 ) = 𝐹 → ( ( ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) ↾ 𝐴 ) : 𝐴 –1-1→ ( On ∖ 𝐵 ) ↔ 𝐹 : 𝐴 –1-1→ ( On ∖ 𝐵 ) ) )
13 11 12 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ( 𝑥 ∈ On ↦ ( 𝐵 +o 𝑥 ) ) ↾ 𝐴 ) : 𝐴 –1-1→ ( On ∖ 𝐵 ) ↔ 𝐹 : 𝐴 –1-1→ ( On ∖ 𝐵 ) ) )
14 9 13 mpbid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : 𝐴 –1-1→ ( On ∖ 𝐵 ) )
15 f1f1orn ⊢ ( 𝐹 : 𝐴 –1-1→ ( On ∖ 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
16 14 15 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
17 f1f ⊢ ( 𝐹 : 𝐴 –1-1→ ( On ∖ 𝐵 ) → 𝐹 : 𝐴 ⟶ ( On ∖ 𝐵 ) )
18 frn ⊢ ( 𝐹 : 𝐴 ⟶ ( On ∖ 𝐵 ) → ran 𝐹 ⊆ ( On ∖ 𝐵 ) )
19 14 17 18 3syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ran 𝐹 ⊆ ( On ∖ 𝐵 ) )
20 19 difss2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ran 𝐹 ⊆ On )
21 reldisj ⊢ ( ran 𝐹 ⊆ On → ( ( ran 𝐹 ∩ 𝐵 ) = ∅ ↔ ran 𝐹 ⊆ ( On ∖ 𝐵 ) ) )
22 20 21 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ran 𝐹 ∩ 𝐵 ) = ∅ ↔ ran 𝐹 ⊆ ( On ∖ 𝐵 ) ) )
23 19 22 mpbird ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ran 𝐹 ∩ 𝐵 ) = ∅ )
24 16 23 jca ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ∧ ( ran 𝐹 ∩ 𝐵 ) = ∅ ) )