Theorem dfhe3

Description: The property of relation R being hereditary in class A . (Contributed by RP, 27-Mar-2020)

	Ref	Expression
Assertion	dfhe3	⊢ ( 𝑅 hereditary 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-he	⊢ ( 𝑅 hereditary 𝐴 ↔ ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )
2		19.21v	⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )
3	2	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )
4	3	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )
5		alcom	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )
6		impexp	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )
7	6	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) )
8	7	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) )
9		19.23v	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) )
10	8 9	bitri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) )
11	10	albii	⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ ∀ 𝑦 ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) )
12	4 5 11	3bitri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ ∀ 𝑦 ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) )
13		dfss2	⊢ ( { 𝑧 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) } ⊆ 𝐴 ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) } → 𝑦 ∈ 𝐴 ) )
14		vex	⊢ 𝑦 ∈ V
15		opeq2	⊢ ( 𝑧 = 𝑦 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
16	15	eleq1d	⊢ ( 𝑧 = 𝑦 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
17		df-br	⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
18	16 17	bitr4di	⊢ ( 𝑧 = 𝑦 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ↔ 𝑥 𝑅 𝑦 ) )
19	18	anbi2d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
20	19	exbidv	⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
21	14 20	elab	⊢ ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
22	21	imbi1i	⊢ ( ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) } → 𝑦 ∈ 𝐴 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) )
23	22	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) } → 𝑦 ∈ 𝐴 ) ↔ ∀ 𝑦 ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) )
24	13 23	bitr2i	⊢ ( ∀ 𝑦 ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) ↔ { 𝑧 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) } ⊆ 𝐴 )
25		dfima3	⊢ ( 𝑅 “ 𝐴 ) = { 𝑧 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) }
26	25	eqcomi	⊢ { 𝑧 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) } = ( 𝑅 “ 𝐴 )
27	26	sseq1i	⊢ ( { 𝑧 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) } ⊆ 𝐴 ↔ ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )
28	24 27	bitri	⊢ ( ∀ 𝑦 ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝐴 ) ↔ ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )
29	12 28	bitr2i	⊢ ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )
30	1 29	bitri	⊢ ( 𝑅 hereditary 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )